[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
z : α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓝[s] z, p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s
[PROOFSTEP]
simp only [Filter.Frequently, eventually_nhdsWithin_iff, not_and']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[{z}ᶜ] z, x ∈ s
[PROOFSTEP]
simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x
[PROOFSTEP]
simp only [eventually_nhdsWithin_iff] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
[PROOFSTEP]
exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a
[PROOFSTEP]
rw [nhdsWithin, principal_univ, inf_top_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
[PROOFSTEP]
simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x
[PROOFSTEP]
rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ
[PROOFSTEP]
exact inter_mem_inf hs (mem_principal_self _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a
[PROOFSTEP]
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w✝ : Set α
Hw : w✝ ∈ 𝓝 a
hw : w✝ ∩ s ⊆ t
⊢ t ∈ 𝓝 a
[PROOFSTEP]
exact (nhds a).sets_of_superset ((nhds a).inter_sets Hw h1) hw
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
[PROOFSTEP]
simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a
[PROOFSTEP]
lift a to t using h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (π ↑a)
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
[PROOFSTEP]
replace hs : (fun x : t => π x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
[PROOFSTEP]
rwa [← map_nhds_subtype_val, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
[PROOFSTEP]
apply nhdsWithin_le_of_mem
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a
[PROOFSTEP]
exact univ_mem
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a
[PROOFSTEP]
rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a
[PROOFSTEP]
rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a
[PROOFSTEP]
rw [← ht.nhdsWithin_eq h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a
[PROOFSTEP]
exact preimage_nhdsWithin_coinduced' h hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[∅] a = ⊥
[PROOFSTEP]
rw [nhdsWithin, principal_empty, inf_bot_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a
[PROOFSTEP]
delta nhdsWithin
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
[PROOFSTEP]
rw [← inf_sup_left, sup_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : Set.Finite I
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι) (_ : i ∈ ∅), s i] a = ⨆ (i : ι) (_ : i ∈ ∅), 𝓝[s i] a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : Set.Finite I
s : ι → Set α
a : α
a✝ : ι
s✝ : Set ι
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
hT : 𝓝[⋃ (i : ι) (_ : i ∈ s✝), s i] a = ⨆ (i : ι) (_ : i ∈ s✝), 𝓝[s i] a
⊢ 𝓝[⋃ (i : ι) (_ : i ∈ insert a✝ s✝), s i] a = ⨆ (i : ι) (_ : i ∈ insert a✝ s✝), 𝓝[s i] a
[PROOFSTEP]
simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : Set.Finite S
a : α
⊢ 𝓝[⋃₀ S] a = ⨆ (s : Set α) (_ : s ∈ S), 𝓝[s] a
[PROOFSTEP]
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
ι : Sort u_5
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a
[PROOFSTEP]
rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a
[PROOFSTEP]
delta nhdsWithin
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
[PROOFSTEP]
rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t
[PROOFSTEP]
delta nhdsWithin
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
[PROOFSTEP]
rw [← inf_principal, inf_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a
[PROOFSTEP]
rw [nhdsWithin_inter, inf_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a
[PROOFSTEP]
exact nhdsWithin_le_of_mem h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a
[PROOFSTEP]
rw [inter_comm, nhdsWithin_inter_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}] a = pure a
[PROOFSTEP]
rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
[PROOFSTEP]
rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ insert a t ∈ 𝓝[insert a s] a
[PROOFSTEP]
simp [mem_of_superset h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[{a}ᶜ] a
[PROOFSTEP]
simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left, insert_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}ᶜ] a ⊔ pure a = 𝓝 a
[PROOFSTEP]
rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : TopologicalSpace α
β : Type u_6
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)
[PROOFSTEP]
rw [nhdsWithin_prod_eq]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : TopologicalSpace α
β : Type u_6
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
[PROOFSTEP]
exact prod_mem_prod hu hv
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi I s] x = ⨅ (i : ι), comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))
[PROOFSTEP]
simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ← iInf_principal_finite hI, ←
  iInf_inf_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi I s] x =
    (⨅ (i : ι) (_ : i ∈ I), comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ (i : ι) (_ : ¬i ∈ I), comap (fun x => x i) (𝓝 (x i))
[PROOFSTEP]
simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf, comap_principal, eval]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ (⨅ (i : ι), comap (fun f => f i) (𝓝 (x i))) ⊓ ⨅ (i : ι) (_ : i ∈ I), 𝓟 ((fun f => f i) ⁻¹' s i) =
    (⨅ (i : ι) (_ : i ∈ I), comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι) (_ : ¬i ∈ I), comap (fun x => x i) (𝓝 (x i))
[PROOFSTEP]
rw [iInf_split _ fun i => i ∈ I, inf_right_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
hI : Set.Finite I
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ ((⨅ (i : ι) (_ : i ∈ I), comap (fun f => f i) (𝓝 (x i))) ⊓ ⨅ (i : ι) (_ : i ∈ I), 𝓟 ((fun f => f i) ⁻¹' s i)) ⊓
      ⨅ (i : ι) (_ : ¬i ∈ I), comap (fun f => f i) (𝓝 (x i)) =
    (⨅ (i : ι) (_ : i ∈ I), comap (fun x => x i) (𝓝 (x i)) ⊓ 𝓟 ((fun x => x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι) (_ : ¬i ∈ I), comap (fun x => x i) (𝓝 (x i))
[PROOFSTEP]
simp only [iInf_inf_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝¹ : Finite ι
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi univ s] x = ⨅ (i : ι), comap (fun x => x i) (𝓝[s i] x i)
[PROOFSTEP]
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ 𝓝[Set.pi I s] x = ⊥ ↔ ∃ i, i ∈ I ∧ 𝓝[s i] x i = ⊥
[PROOFSTEP]
simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ NeBot (𝓝[Set.pi I s] x) ↔ ∀ (i : ι), i ∈ I → NeBot (𝓝[s i] x i)
[PROOFSTEP]
simp [neBot_iff, nhdsWithin_pi_eq_bot]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto (piecewise t f g) (𝓝[s] a) l
[PROOFSTEP]
apply Tendsto.piecewise
[GOAL]
case h₀
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto f (𝓝[s] a ⊓ 𝓟 t) l
[PROOFSTEP]
rwa [← nhdsWithin_inter']
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l
[PROOFSTEP]
rwa [← nhdsWithin_inter']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s
[PROOFSTEP]
simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff, eventually_and] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen i → (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s
[PROOFSTEP]
exact (h univ ⟨mem_univ a, isOpen_univ⟩).2
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α✝
α : Type u_5
s : Set α
t : Set ↑s
⊢ 𝓟 t = comap Subtype.val (𝓟 (Subtype.val '' t))
[PROOFSTEP]
rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ closure (Set.pi I s) ↔ ∀ (i : ι), i ∈ I → x i ∈ closure (s i)
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α✝
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
I : Set ι
hs : ∀ (i : ι), i ∈ I → Dense (s i)
⊢ Dense (Set.pi I s)
[PROOFSTEP]
simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq, pi_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
[PROOFSTEP]
rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a
[PROOFSTEP]
rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
a : ↑s
⊢ Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a
[PROOFSTEP]
rw [← map_nhds_subtype_val, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (restrict s f) (𝓝 { val := a, property := h }) l
[PROOFSTEP]
rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto (f ∘ Subtype.val) (𝓝 { val := a, property := h }) l ↔ Tendsto (restrict s f) (𝓝 { val := a, property := h }) l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
x : α
⊢ ContinuousWithinAt f univ x ↔ ContinuousAt f x
[PROOFSTEP]
rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g t y
⊢ ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
[PROOFSTEP]
unfold ContinuousWithinAt at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s ×ˢ t] (x, y)) (𝓝 (Prod.map f g (x, y)))
[PROOFSTEP]
rw [nhdsWithin_prod_eq, Prod.map, nhds_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → γ
g : β → δ
s : Set α
t : Set β
x : α
y : β
hf : Tendsto f (𝓝[s] x) (𝓝 (f x))
hg : Tendsto g (𝓝[t] y) (𝓝 (g y))
⊢ Tendsto (Prod.map f g) (𝓝[s] x ×ˢ 𝓝[t] y) (𝓝 (f x) ×ˢ 𝓝 (g y))
[PROOFSTEP]
exact hf.prod_map hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (x : α), x ∈ s → ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t
[PROOFSTEP]
simp only [ContinuousOn, ContinuousWithinAt, tendsto_nhds, mem_nhdsWithin]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous (restrict s f)
[PROOFSTEP]
rw [ContinuousOn, continuous_iff_continuousAt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (restrict s f) x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (restrict s f) x
[PROOFSTEP]
rintro h ⟨x, xs⟩
[GOAL]
case mp.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (restrict s f) { val := x, property := xs }
[PROOFSTEP]
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mp (h x xs)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (restrict s f) x) → ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
[PROOFSTEP]
intro h x xs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (restrict s f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mpr (h ⟨x, xs⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
have : ∀ t, IsOpen (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
  by
  intro t
  rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
  simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
  constructor <;>
    · rintro ⟨u, ou, useq⟩
      exact ⟨u, ou, useq.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ∀ (t : Set β), IsOpen (restrict s f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
intro t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ IsOpen (restrict s f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
rw [isOpen_induced_iff, Set.restrict_eq, Set.preimage_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' (f ⁻¹' t)) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
simp only [Subtype.preimage_coe_eq_preimage_coe_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ t_1 ∩ s = f ⁻¹' t ∩ s) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen t_1 ∧ t_1 ∩ s = f ⁻¹' t ∩ s) → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
rintro ⟨u, ou, useq⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen u
useq : u ∩ s = f ⁻¹' t ∩ s
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
exact ⟨u, ou, useq.symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ t_1, IsOpen t_1 ∧ t_1 ∩ s = f ⁻¹' t ∩ s
[PROOFSTEP]
rintro ⟨u, ou, useq⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ t_1, IsOpen t_1 ∧ t_1 ∩ s = f ⁻¹' t ∩ s
[PROOFSTEP]
exact ⟨u, ou, useq.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsOpen (restrict s f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict, continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsOpen (restrict s f ⁻¹' t) ↔ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β), IsOpen s_1 → IsOpen (restrict s f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
simp only [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
  by
  intro t
  rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
  simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
intro t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsClosed t_1 ∧ Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' (f ⁻¹' t)) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
this : ∀ (t : Set β), IsClosed (restrict s f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ (∀ (s_1 : Set β), IsClosed s_1 → IsClosed (restrict s f ⁻¹' s_1)) ↔
    ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
simp only [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
ι : Sort u_5
f : α → β
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ ContinuousAt f x
[PROOFSTEP]
rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
ι : Sort u_5
f : α → β
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))
[PROOFSTEP]
exact hf _ _ (mem_of_mem_nhds hi)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
a : α
⊢ ContinuousWithinAt f {a} a
[PROOFSTEP]
simpa only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_left] using fun s => mem_of_mem_nhds
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
⊢ Continuous f ↔ ContinuousOn f univ
[PROOFSTEP]
simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
x : α
s t : Set α
f : α → β
h : 𝓝[s] x = 𝓝[t] x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
[PROOFSTEP]
simp only [ContinuousWithinAt, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
[PROOFSTEP]
simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝 x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
[PROOFSTEP]
simp [ContinuousWithinAt, nhdsWithin_restrict' s h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
⊢ ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x
[PROOFSTEP]
simp only [ContinuousWithinAt, nhdsWithin_union, tendsto_sup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
x : α
⊢ ContinuousWithinAt f {x} x
[PROOFSTEP]
simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
x : α
s : Set α
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
[PROOFSTEP]
simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
ht : ContinuousWithinAt f t x
h : ContinuousWithinAt f (s \ t) x
⊢ s ⊆ s \ t ∪ t
[PROOFSTEP]
simp only [diff_union_self, subset_union_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
a : α
⊢ ContinuousWithinAt f {a}ᶜ a ↔ ContinuousAt f a
[PROOFSTEP]
rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : DecidableEq α
f : α → β
s : Set α
x : α
y : β
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)
[PROOFSTEP]
{rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_same]
}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : DecidableEq α
f : α → β
s : Set α
x : α
y : β
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)
[PROOFSTEP]
rw [← continuousWithinAt_diff_self, ContinuousWithinAt, update_same]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : DecidableEq α
f : α → β
x : α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[{x}ᶜ] x) (𝓝 y)
[PROOFSTEP]
rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)
[PROOFSTEP]
refine' continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (f '' (t ∩ s))
[PROOFSTEP]
rw [← image_restrict]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (Set.restrict s f '' (Subtype.val ⁻¹' t))
[PROOFSTEP]
exact h _ (ht.preimage continuous_subtype_val)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
[PROOFSTEP]
rw [inter_eq_self_of_subset_left (image_subset f (inter_subset_right t s)), hleft.image_inter']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (range f)
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : IsOpenMap f
finv : β → α
hleft : LeftInverse finv f
⊢ ContinuousOn finv (f '' univ)
[PROOFSTEP]
exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
⊢ ContinuousOn g s₁
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ ContinuousWithinAt g s₁ x
[PROOFSTEP]
unfold ContinuousWithinAt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
[PROOFSTEP]
have A := (h x (h₁ hx)).mono h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : ContinuousWithinAt f s₁ x
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
[PROOFSTEP]
unfold ContinuousWithinAt at A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (f x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
[PROOFSTEP]
rw [← h' hx] at A
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
[PROOFSTEP]
exact A.congr' h'.eventuallyEq_nhdsWithin.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x
[PROOFSTEP]
rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : Continuous f
⊢ ContinuousOn f s
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s
[PROOFSTEP]
exact h.mono (subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous f
hs : ∀ (x : α), f x ∈ s
⊢ Continuous (g ∘ f)
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : ContinuousOn f univ
hs : ∀ (x : α), f x ∈ s
⊢ ContinuousOn (g ∘ f) univ
[PROOFSTEP]
exact hg.comp hf fun x _ => hs x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) ≤ 𝓝[g '' s] g x
[PROOFSTEP]
exact hg.tendsto_nhdsWithin (mapsTo_image _ _)
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
[PROOFSTEP]
have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id := h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ 𝓝[g '' s] g x ≤ map g (𝓝[s] x)
[PROOFSTEP]
refine' le_map_of_right_inverse A _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
A : g ∘ f =ᶠ[𝓝[g '' s] g x] id
⊢ Tendsto f (𝓝[g '' s] g x) (𝓝[s] x)
[PROOFSTEP]
simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x
[PROOFSTEP]
simpa only [nhdsWithin_univ, image_univ] using
  (h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)
[PROOFSTEP]
rwa [image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α → β
s : Set α
x : α
h : f =ᶠ[𝓝[s] x] g
hx : f x = g x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
[PROOFSTEP]
rw [ContinuousWithinAt, hx, tendsto_congr' h, ContinuousWithinAt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [continuousOn_iff']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
[PROOFSTEP]
intro h t ht
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
⊢ IsOpen (s ∩ f ⁻¹' t)
[PROOFSTEP]
rcases h t ht with ⟨u, u_open, hu⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [inter_comm, hu]
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ IsOpen (u ∩ s)
[PROOFSTEP]
apply IsOpen.inter u_open hs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
⊢ (∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)) → ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
intro h t ht
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
[PROOFSTEP]
refine' ⟨s ∩ f ⁻¹' t, h t ht, _⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
hs : IsOpen s
h : ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
t : Set β
ht : IsOpen t
⊢ f ⁻¹' t ∩ s = s ∩ f ⁻¹' t ∩ s
[PROOFSTEP]
rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ IsOpen (f ⁻¹' t)
[PROOFSTEP]
convert (continuousOn_open_iff hs).mp h t ht
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t
[PROOFSTEP]
rw [inter_comm, inter_eq_self_of_subset_left hp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
⊢ IsClosed (s ∩ f ⁻¹' t)
[PROOFSTEP]
rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [inter_comm, hu.2]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (u ∩ s)
[PROOFSTEP]
apply IsClosed.inter hu.1 hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsOpen s
⊢ interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
[PROOFSTEP]
rw [interior_inter, hs.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s
[PROOFSTEP]
intro x xs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rcases h x xs with ⟨t, open_t, xt, ct⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
have := ct x ⟨xs, xt⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
[PROOFSTEP]
delta ContinuousWithinAt
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
[PROOFSTEP]
simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
[PROOFSTEP]
exact forall_congr' fun t => forall_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
s : Set α
x : α
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
[PROOFSTEP]
simp_rw [ContinuousWithinAt, Inducing.tendsto_nhds_iff hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
s : Set α
x : α
⊢ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 (g (f x))) ↔ Tendsto (g ∘ f) (𝓝[s] x) (𝓝 ((g ∘ f) x))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
[PROOFSTEP]
simp_rw [ContinuousOn, hg.continuousWithinAt_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : _root_.Embedding f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x
[PROOFSTEP]
rw [nhdsWithin, Filter.map_inf hf.inj, hf.map_nhds_eq, map_principal, ← nhdsWithin_inter',
  inter_eq_self_of_subset_right (image_subset_range _ _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
[PROOFSTEP]
rw [hf.toEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
[PROOFSTEP]
apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.open_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f
[PROOFSTEP]
rw [inter_assoc, inter_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
⊢ ¬x ∈ closure s → ContinuousWithinAt f s x
[PROOFSTEP]
intro hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : ¬x ∈ closure s
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rw [mem_closure_iff_nhdsWithin_neBot, neBot_iff, not_not] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x
[PROOFSTEP]
rw [ContinuousWithinAt, hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))
[PROOFSTEP]
exact tendsto_bot
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
⊢ ContinuousOn (fun a => if p a then f a else g a) s
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
[PROOFSTEP]
by_cases hx' : x ∈ frontier {a | p a}
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
[PROOFSTEP]
exact (hpf x ⟨hx, hx'⟩).piecewise_nhdsWithin (hpg x ⟨hx, hx'⟩)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) s x
[PROOFSTEP]
rw [← inter_univ s, ← union_compl_self {a | p a}, inter_union_distrib_left] at hx ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : ¬x ∈ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case neg.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
apply ContinuousWithinAt.union
[GOAL]
case neg.inl.hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
[PROOFSTEP]
exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)
[GOAL]
case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
have : x ∉ closure {a | p a}ᶜ := fun h => hx' ⟨subset_closure hx.2, by rwa [closure_compl] at h ⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ closure {a | p a}ᶜ
⊢ ¬x ∈ interior {a | p a}
[PROOFSTEP]
rwa [closure_compl] at h
[GOAL]
case neg.inl.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : ¬x ∈ closure {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
exact continuousWithinAt_of_not_mem_closure fun h => this (closure_inter_subset_inter_closure _ _ h).2
[GOAL]
case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
apply ContinuousWithinAt.union
[GOAL]
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
[PROOFSTEP]
have : x ∉ closure {a | p a} := fun h => hx' ⟨h, fun h' : x ∈ interior {a | p a} => hx.2 (interior_subset h')⟩
[GOAL]
case neg.inr.hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
this : ¬x ∈ closure {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}) x
[PROOFSTEP]
exact continuousWithinAt_of_not_mem_closure fun h => this (closure_inter_subset_inter_closure _ _ h).2
[GOAL]
case neg.inr.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : ¬x ∈ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
[PROOFSTEP]
exact (hg x hx).congr (fun y hy => if_neg hy.2) (if_neg hx.2)
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => if p a then f a else g a) s
[PROOFSTEP]
apply ContinuousOn.if'
[GOAL]
case hpf
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
rintro a ha
[GOAL]
case hpf
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
simp only [← hp a ha, ite_self]
[GOAL]
case hpf
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ {a | p a}] a) (𝓝 (f a))
[PROOFSTEP]
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
[GOAL]
case hpf
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => f a) (𝓝[s ∩ closure {a | p a}] a) (𝓝 (f a))
[PROOFSTEP]
exact hf a ⟨ha.1, ha.2.1⟩
[GOAL]
case hpg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
rintro a ha
[GOAL]
case hpg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
simp only [hp a ha, ite_self]
[GOAL]
case hpg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (g a))
[PROOFSTEP]
apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
[GOAL]
case hpg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
[PROOFSTEP]
rcases ha with ⟨has, ⟨_, ha⟩⟩
[GOAL]
case hpg.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : ¬a ∈ interior {a | p a}
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
[PROOFSTEP]
rw [← mem_compl_iff, ← closure_compl] at ha
[GOAL]
case hpg.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
a : α
has : a ∈ s
left✝ : a ∈ closure {a | p a}
ha : a ∈ closure {a | p a}ᶜ
⊢ Tendsto (fun a => g a) (𝓝[s ∩ closure {a | ¬p a}] a) (𝓝 (g a))
[PROOFSTEP]
apply hg a ⟨has, ha⟩
[GOAL]
case hf
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => f a) (s ∩ {a | p a})
[PROOFSTEP]
exact hf.mono (inter_subset_inter_right s subset_closure)
[GOAL]
case hg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : TopologicalSpace α✝
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : TopologicalSpace γ
inst✝³ : TopologicalSpace δ
α : Type u_5
β : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
s : Set α
f g : α → β
hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a
hf : ContinuousOn f (s ∩ closure {a | p a})
hg : ContinuousOn g (s ∩ closure {a | ¬p a})
⊢ ContinuousOn (fun a => g a) (s ∩ {a | ¬p a})
[PROOFSTEP]
exact hg.mono (inter_subset_inter_right s subset_closure)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ Continuous fun a => if p a then f a else g a
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a => if p a then f a else g a) univ
[PROOFSTEP]
apply ContinuousOn.if'
[GOAL]
case hpf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ (a : α),
    a ∈ univ ∩ frontier {a | p a} → Tendsto (fun a => f a) (𝓝[univ ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
simp [*]
[GOAL]
case hpg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ (a : α),
    a ∈ univ ∩ frontier {a | p a} → Tendsto (fun a => g a) (𝓝[univ ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
simp [*]
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a => f a) (univ ∩ {a | p a})
[PROOFSTEP]
simp [*]
[GOAL]
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ContinuousOn (fun a => g a) (univ ∩ {a | ¬p a})
[PROOFSTEP]
simp [*]
[GOAL]
case hpf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ (a : α), a ∈ frontier {a | p a} → Tendsto (fun a => f a) (𝓝[{a | p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
assumption
[GOAL]
case hpg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ (a : α), a ∈ frontier {x | p x} → Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x | p x}
hg : ContinuousOn g {x | ¬p x}
⊢ ∀ (a : α), a ∈ frontier {a | p a} → Tendsto (fun a => g a) (𝓝[{a | ¬p a}] a) (𝓝 (if p a then f a else g a))
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ Continuous fun a => if p a then f a else g a
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => if p a then f a else g a) univ
[PROOFSTEP]
apply ContinuousOn.if
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ∀ (a : α), a ∈ univ ∩ frontier {a | p a} → f a = g a
[PROOFSTEP]
simp
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => f a) (univ ∩ closure {a | p a})
[PROOFSTEP]
simp
[GOAL]
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => g a) (univ ∩ closure {a | ¬p a})
[PROOFSTEP]
simp
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ∀ (a : α), a ∈ frontier {a | p a} → f a = g a
[PROOFSTEP]
assumption
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => f a) (closure {a | p a})
[PROOFSTEP]
assumption
[GOAL]
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => g a) (closure {a | ¬p a})
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
⊢ Continuous fun a => if p then f a else g a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : p
⊢ Continuous fun a => f a
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
p : Prop
f g : α → β
inst✝ : Decidable p
hf : p → Continuous f
hg : ¬p → Continuous g
h : ¬p
⊢ Continuous fun a => g a
[PROOFSTEP]
exacts [hf h, hg h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
⊢ IsOpen (Set.ite t s s')
[PROOFSTEP]
classical
simp only [isOpen_iff_continuous_mem, Set.ite] at *
convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn
rename_i x
by_cases hx : x ∈ t <;> simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
⊢ IsOpen (Set.ite t s s')
[PROOFSTEP]
simp only [isOpen_iff_continuous_mem, Set.ite] at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
⊢ Continuous fun x => x ∈ s ∩ t ∪ s' \ t
[PROOFSTEP]
convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn
[GOAL]
case h.e'_5.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x✝
[PROOFSTEP]
rename_i x
[GOAL]
case h.e'_5.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x
[PROOFSTEP]
by_cases hx : x ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
hx : ¬x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'
[PROOFSTEP]
simpa [hx] using ext_iff.1 ht x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ Set.ite t s s' ∩ closure t = s ∩ closure t
[PROOFSTEP]
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left, ite_inter_self,
  ite_inter_of_inter_eq _ ht]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ Set.ite t s s' ∩ closure tᶜ = s' ∩ closure tᶜ
[PROOFSTEP]
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ
[PROOFSTEP]
rwa [frontier_compl, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn (piecewise t f f') (Set.ite t s s')
[PROOFSTEP]
apply ContinuousOn.piecewise
[GOAL]
case ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ∀ (a : α), a ∈ Set.ite t s s' ∩ frontier t → f a = f' a
[PROOFSTEP]
rwa [ite_inter_of_inter_eq _ H]
[GOAL]
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f (Set.ite t s s' ∩ closure t)
[PROOFSTEP]
rwa [ite_inter_closure_eq_of_inter_frontier_eq H]
[GOAL]
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f' (Set.ite t s s' ∩ closure tᶜ)
[PROOFSTEP]
rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s t : Set α
ht : IsOpen t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t
[PROOFSTEP]
simp only [← Subtype.preimage_coe_eq_preimage_coe_iff,
  ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
  Subtype.preimage_coe_inter_self]