[GOAL]
α : Type u
T : Set (Set α)
empty_mem : ∅ ∈ T
sInter_mem : ∀ (A : Set (Set α)), A ⊆ T → ⋂₀ A ∈ T
union_mem : ∀ (A : Set α), A ∈ T → ∀ (B : Set α), B ∈ T → A ∪ B ∈ T
⊢ (fun X => Xᶜ ∈ T) univ
[PROOFSTEP]
simp [empty_mem]
[GOAL]
α : Type u
T : Set (Set α)
empty_mem : ∅ ∈ T
sInter_mem : ∀ (A : Set (Set α)), A ⊆ T → ⋂₀ A ∈ T
union_mem : ∀ (A : Set α), A ∈ T → ∀ (B : Set α), B ∈ T → A ∪ B ∈ T
s t : Set α
hs : (fun X => Xᶜ ∈ T) s
ht : (fun X => Xᶜ ∈ T) t
⊢ (fun X => Xᶜ ∈ T) (s ∩ t)
[PROOFSTEP]
simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht
[GOAL]
α : Type u
T : Set (Set α)
empty_mem : ∅ ∈ T
sInter_mem : ∀ (A : Set (Set α)), A ⊆ T → ⋂₀ A ∈ T
union_mem : ∀ (A : Set α), A ∈ T → ∀ (B : Set α), B ∈ T → A ∪ B ∈ T
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → (fun X => Xᶜ ∈ T) t
⊢ (fun X => Xᶜ ∈ T) (⋃₀ s)
[PROOFSTEP]
simp only [Set.compl_sUnion]
[GOAL]
α : Type u
T : Set (Set α)
empty_mem : ∅ ∈ T
sInter_mem : ∀ (A : Set (Set α)), A ⊆ T → ⋂₀ A ∈ T
union_mem : ∀ (A : Set α), A ∈ T → ∀ (B : Set α), B ∈ T → A ∪ B ∈ T
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → (fun X => Xᶜ ∈ T) t
⊢ ⋂₀ (compl '' s) ∈ T
[PROOFSTEP]
exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
t t' : TopologicalSpace α
h : ∀ (s : Set α), IsOpen s ↔ IsOpen s
⊢ t = t'
[PROOFSTEP]
ext
[GOAL]
case a.h.a
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
t t' : TopologicalSpace α
h : ∀ (s : Set α), IsOpen s ↔ IsOpen s
x✝ : Set α
⊢ IsOpen x✝ ↔ IsOpen x✝
[PROOFSTEP]
exact h _
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (s₁ ∪ s₂)
[PROOFSTEP]
rw [union_eq_iUnion]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (⋃ (b : Bool), bif b then s₁ else s₂)
[PROOFSTEP]
exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ IsOpen ∅
[PROOFSTEP]
rw [← sUnion_empty]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ IsOpen (⋃₀ ∅)
[PROOFSTEP]
exact isOpen_sUnion fun a => False.elim
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
x✝ : ∀ (t : Set α), t ∈ ∅ → IsOpen t
⊢ IsOpen (⋂₀ ∅)
[PROOFSTEP]
rw [sInter_empty]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
x✝ : ∀ (t : Set α), t ∈ ∅ → IsOpen t
⊢ IsOpen univ
[PROOFSTEP]
exact isOpen_univ
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
ih : (∀ (t : Set α), t ∈ s✝ → IsOpen t) → IsOpen (⋂₀ s✝)
h : ∀ (t : Set α), t ∈ insert a✝ s✝ → IsOpen t
⊢ IsOpen (⋂₀ insert a✝ s✝)
[PROOFSTEP]
simp only [sInter_insert, ball_insert_iff] at h ⊢
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : Set.Finite s
a✝ : Set α
s✝ : Set (Set α)
x✝¹ : ¬a✝ ∈ s✝
x✝ : Set.Finite s✝
ih : (∀ (t : Set α), t ∈ s✝ → IsOpen t) → IsOpen (⋂₀ s✝)
h : IsOpen a✝ ∧ ∀ (x : Set α), x ∈ s✝ → IsOpen x
⊢ IsOpen (a✝ ∩ ⋂₀ s✝)
[PROOFSTEP]
exact h.1.inter (ih h.2)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : Prop
⊢ IsOpen {_a | p}
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : Prop
⊢ IsOpen {_a | p}
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : Prop
h : p
⊢ IsOpen {_a | p}
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : Prop
h : ¬p
⊢ IsOpen {_a | p}
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)
[PROOFSTEP]
simpa only [← isOpen_compl_iff, compl_union] using IsOpen.inter
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set (Set α)
⊢ (∀ (t : Set α), t ∈ s → IsClosed t) → IsClosed (⋂₀ s)
[PROOFSTEP]
simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed sᶜ ↔ IsOpen s
[PROOFSTEP]
rw [← isOpen_compl_iff, compl_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ IsClosed (s₁ ∩ s₂)
[PROOFSTEP]
rw [← isOpen_compl_iff] at *
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ ∩ s₂)ᶜ
[PROOFSTEP]
rw [compl_inter]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁ᶜ
h₂ : IsOpen s₂ᶜ
⊢ IsOpen (s₁ᶜ ∪ s₂ᶜ)
[PROOFSTEP]
exact IsOpen.union h₁ h₂
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set β
f : β → Set α
hs : Set.Finite s
h : ∀ (i : β), i ∈ s → IsClosed (f i)
⊢ IsClosed (⋃ (i : β) (_ : i ∈ s), f i)
[PROOFSTEP]
simp only [← isOpen_compl_iff, compl_iUnion] at *
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set β
f : β → Set α
hs : Set.Finite s
h : ∀ (i : β), i ∈ s → IsOpen (f i)ᶜ
⊢ IsOpen (⋂ (i : β) (_ : i ∈ s), (f i)ᶜ)
[PROOFSTEP]
exact isOpen_biInter hs h
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), IsClosed (s i)
⊢ IsClosed (⋃ (i : ι), s i)
[PROOFSTEP]
simp only [← isOpen_compl_iff, compl_iUnion] at *
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : Finite ι
s : ι → Set α
h : ∀ (i : ι), IsOpen (s i)ᶜ
⊢ IsOpen (⋂ (i : ι), (s i)ᶜ)
[PROOFSTEP]
exact isOpen_iInter h
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p q : α → Prop
hp : IsOpen {x | p x}
hq : IsClosed {x | q x}
⊢ IsClosed {x | p x → q x}
[PROOFSTEP]
simpa only [imp_iff_not_or] using hp.isClosed_compl.union hq
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ interior s ↔ IsOpen s
[PROOFSTEP]
simp only [interior_eq_iff_isOpen.symm, Subset.antisymm_iff, interior_subset, true_and]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ interior (⋂ (i : ι) (_ : i ∈ s), f i) = ⋂ (i : ι) (_ : i ∈ s), interior (f i)
[PROOFSTEP]
classical
refine' s.induction_on (by simp) _
intro i s _ h₂
simp [h₂]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ interior (⋂ (i : ι) (_ : i ∈ s), f i) = ⋂ (i : ι) (_ : i ∈ s), interior (f i)
[PROOFSTEP]
refine' s.induction_on (by simp) _
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ interior (⋂ (i : ι) (_ : i ∈ ∅), f i) = ⋂ (i : ι) (_ : i ∈ ∅), interior (f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      interior (⋂ (i : ι) (_ : i ∈ s), f i) = ⋂ (i : ι) (_ : i ∈ s), interior (f i) →
        interior (⋂ (i : ι) (_ : i ∈ insert a s), f i) = ⋂ (i : ι) (_ : i ∈ insert a s), interior (f i)
[PROOFSTEP]
intro i s _ h₂
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s✝ : Finset ι
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h₂ : interior (⋂ (i : ι) (_ : i ∈ s), f i) = ⋂ (i : ι) (_ : i ∈ s), interior (f i)
⊢ interior (⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), interior (f i_1)
[PROOFSTEP]
simp [h₂]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
⊢ interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
[PROOFSTEP]
convert Finset.univ.interior_iInter f
[GOAL]
case h.e'_2.h.e'_3.h.e'_3.h
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
x✝ : ι
⊢ f x✝ = ⋂ (_ : x✝ ∈ Finset.univ), f x✝
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_3.h
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
x✝ : ι
⊢ interior (f x✝) = ⋂ (_ : x✝ ∈ Finset.univ), interior (f x✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h₁ : IsClosed s
h₂ : interior t = ∅
x : α
x✝ : x ∈ interior (s ∪ t)
u : Set α
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : ¬x ∈ s
this : u \ s ⊆ t
⊢ u \ s ⊆ interior t
[PROOFSTEP]
rwa [(IsOpen.sdiff hu₁ h₁).subset_interior_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h₁ : IsClosed s
h₂ : interior t = ∅
x : α
x✝ : x ∈ interior (s ∪ t)
u : Set α
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : ¬x ∈ s
this✝ : u \ s ⊆ t
this : u \ s ⊆ interior t
⊢ u \ s ⊆ ∅
[PROOFSTEP]
rwa [h₂] at this
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rw [← subset_interior_iff_isOpen]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ s ⊆ interior s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
simp only [subset_def, mem_interior]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
S : Set (Set α)
⊢ interior (⋂₀ S) = interior (⋂ (s : Set α) (_ : s ∈ S), s)
[PROOFSTEP]
rw [sInter_eq_biInter]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t
[PROOFSTEP]
rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : closure s ⊆ s
⊢ IsClosed s
[PROOFSTEP]
rw [subset_closure.antisymm h]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : closure s ⊆ s
⊢ IsClosed (closure s)
[PROOFSTEP]
exact isClosed_closure
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ Set.Nonempty (closure s) ↔ Set.Nonempty s
[PROOFSTEP]
simp only [nonempty_iff_ne_empty, Ne.def, closure_empty_iff]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
[PROOFSTEP]
classical
refine' s.induction_on (by simp) _
intro i s _ h₂
simp [h₂]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
[PROOFSTEP]
refine' s.induction_on (by simp) _
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ closure (⋃ (i : ι) (_ : i ∈ ∅), f i) = ⋃ (i : ι) (_ : i ∈ ∅), closure (f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s : Finset ι
f : ι → Set α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i) →
        closure (⋃ (i : ι) (_ : i ∈ insert a s), f i) = ⋃ (i : ι) (_ : i ∈ insert a s), closure (f i)
[PROOFSTEP]
intro i s _ h₂
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s✝¹ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
s✝ : Finset ι
f : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h₂ : closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)
⊢ closure (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), f i_1) = ⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), closure (f i_1)
[PROOFSTEP]
simp [h₂]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
[PROOFSTEP]
convert Finset.univ.closure_biUnion f
[GOAL]
case h.e'_2.h.e'_3.h.e'_3.h
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
x✝ : ι
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_3.h
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype ι
x✝ : ι
⊢ closure (f x✝) = ⋃ (_ : x✝ ∈ Finset.univ), closure (f x✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s = (interior sᶜ)ᶜ
[PROOFSTEP]
rw [interior, closure, compl_sUnion, compl_image_set_of]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}
[PROOFSTEP]
simp only [compl_subset_compl, isOpen_compl_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ interior sᶜ = (closure s)ᶜ
[PROOFSTEP]
simp [closure_eq_compl_interior_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure sᶜ = (interior s)ᶜ
[PROOFSTEP]
simp [closure_eq_compl_interior_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
l : Filter α
h : l = ⊥
⊢ Filter.lift' ⊥ closure = ⊥
[PROOFSTEP]
rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ interior s = ∅ ↔ Dense sᶜ
[PROOFSTEP]
rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
⊢ Dense sᶜᶜ
[PROOFSTEP]
rwa [compl_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ Dense (closure s) ↔ Dense s
[PROOFSTEP]
rw [Dense, Dense, closure_closure]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ Dense s ↔ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ Dense s → ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)) → Dense s
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
⊢ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
[PROOFSTEP]
rintro U U_op ⟨x, x_in⟩
[GOAL]
case mp.intro
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : Dense s
U : Set α
U_op : IsOpen U
x : α
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
[PROOFSTEP]
exact mem_closure_iff.1 (h _) U U_op x_in
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
⊢ Dense s
[PROOFSTEP]
intro x
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ x ∈ closure s
[PROOFSTEP]
rw [mem_closure_iff]
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
⊢ ∀ (o : Set α), IsOpen o → x ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
intro U U_op x_in
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)
x : α
U : Set α
U_op : IsOpen U
x_in : x ∈ U
⊢ Set.Nonempty (U ∩ s)
[PROOFSTEP]
exact h U U_op ⟨_, x_in⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
⊢ Dense {x}ᶜ ↔ ¬IsOpen {x}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
⊢ Dense {x}ᶜ → ¬IsOpen {x}
[PROOFSTEP]
intro hd ho
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ False
[PROOFSTEP]
exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
⊢ ¬IsOpen {x} → Dense {x}ᶜ
[PROOFSTEP]
refine' fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => _
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
ho : ¬IsOpen {x}
U : Set α
hU : IsOpen U
hne : Set.Nonempty U
hUx : U ⊆ {x}
⊢ False
[PROOFSTEP]
obtain rfl : U = { x }
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
ho : ¬IsOpen {x}
U : Set α
hU : IsOpen U
hne : Set.Nonempty U
hUx : U ⊆ {x}
⊢ U = {x}
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
ho : ¬IsOpen {x}
hU : IsOpen {x}
hne : Set.Nonempty {x}
hUx : {x} ⊆ {x}
⊢ False
[PROOFSTEP]
exact eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
ho : ¬IsOpen {x}
hU : IsOpen {x}
hne : Set.Nonempty {x}
hUx : {x} ⊆ {x}
⊢ False
[PROOFSTEP]
exact ho hU
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s \ frontier s = interior s
[PROOFSTEP]
rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s \ frontier s = interior s
[PROOFSTEP]
rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure, inter_eq_self_of_subset_right interior_subset,
  empty_union]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier s = closure s ∩ closure sᶜ
[PROOFSTEP]
rw [closure_compl, frontier, diff_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier sᶜ = frontier s
[PROOFSTEP]
simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ frontier univ = ∅
[PROOFSTEP]
simp [frontier]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
⊢ frontier ∅ = ∅
[PROOFSTEP]
simp [frontier]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
[PROOFSTEP]
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
[PROOFSTEP]
refine' (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq _
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
[PROOFSTEP]
simp only [inter_distrib_left, inter_distrib_right, inter_assoc, inter_comm (closure t)]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
[PROOFSTEP]
simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
⊢ frontier s = s \ interior s
[PROOFSTEP]
rw [frontier, hs.closure_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ frontier s = closure s \ s
[PROOFSTEP]
rw [frontier, hs.interior_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ s ∩ frontier s = ∅
[PROOFSTEP]
rw [hs.frontier_eq, inter_diff_self]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed (frontier s)
[PROOFSTEP]
rw [frontier_eq_closure_inter_closure]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed (closure s ∩ closure sᶜ)
[PROOFSTEP]
exact IsClosed.inter isClosed_closure isClosed_closure
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
⊢ interior (frontier s) = ∅
[PROOFSTEP]
have A : frontier s = s \ interior s := h.frontier_eq
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅
[PROOFSTEP]
have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono (diff_subset _ _)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) ⊆ interior s
[PROOFSTEP]
rw [A]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s
[PROOFSTEP]
exact interior_mono (diff_subset _ _)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) = ∅
[PROOFSTEP]
have C : interior (frontier s) ⊆ frontier s := interior_subset
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) = ∅
[PROOFSTEP]
have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) := subset_inter B (by simpa [A] using C)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ s \ interior s
[PROOFSTEP]
simpa [A] using C
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅
[PROOFSTEP]
rwa [inter_diff_self, subset_empty_iff] at this
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
[PROOFSTEP]
rw [← frontier_compl, ← closure_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ (frontier s)ᶜ = interior s ∪ interior sᶜ
[PROOFSTEP]
rw [frontier_eq_inter_compl_interior]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ
[PROOFSTEP]
simp only [compl_inter, compl_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a = ⨅ (s : Set α) (_ : IsOpen s) (_ : a ∈ s), 𝓟 s
[PROOFSTEP]
simp only [nhds_def, mem_setOf_eq, @and_comm (a ∈ _), iInf_and]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (𝓝 a) (fun s => a ∈ s ∧ IsOpen s) fun s => s
[PROOFSTEP]
rw [nhds_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) (fun s => a ∈ s ∧ IsOpen s) fun s => s
[PROOFSTEP]
exact
  hasBasis_biInf_principal
    (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
      ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left _ _, inter_subset_right _ _⟩⟩)
    ⟨univ, ⟨mem_univ a, isOpen_univ⟩⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
t : Set α
⊢ (∃ x, (a ∈ xᶜ ∧ IsOpen xᶜ) ∧ xᶜ ⊆ t) ↔ ∃ i, (¬a ∈ i ∧ IsClosed i) ∧ iᶜ ⊆ t
[PROOFSTEP]
simp only [isOpen_compl_iff, mem_compl_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
⊢ f ≤ 𝓝 a ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
[PROOFSTEP]
simp [nhds_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ 𝓝 a ≤ f
[PROOFSTEP]
rw [nhds_def]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s ≤ f
[PROOFSTEP]
exact iInf₂_le_of_le s ⟨h, o⟩ sf
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
p : α → Prop
⊢ (∃ t, t ⊆ {x | (fun x => p x) x} ∧ IsOpen t ∧ a ∈ t) ↔ ∃ t, (∀ (x : α), x ∈ t → p x) ∧ IsOpen t ∧ a ∈ t
[PROOFSTEP]
simp only [subset_def, exists_prop, mem_setOf_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (𝓝 a) (fun s => s ∈ 𝓝 a ∧ IsOpen s) fun x => x
[PROOFSTEP]
convert nhds_basis_opens a using 2
[GOAL]
case h.e'_4.h.a
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
x✝ : Set α
⊢ x✝ ∈ 𝓝 a ∧ IsOpen x✝ ↔ a ∈ x✝ ∧ IsOpen x✝
[PROOFSTEP]
exact and_congr_left_iff.2 IsOpen.mem_nhds_iff
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s U : Set α
h : U ∈ ⨆ (x : α) (_ : x ∈ s), 𝓝 x
⊢ ∀ (x : α), x ∈ s → U ∈ 𝓝 x
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
a : α
⊢ (∃ᶠ (y : α) in 𝓝 a, ∃ᶠ (x : α) in 𝓝 y, p x) ↔ ∃ᶠ (x : α) in 𝓝 a, p x
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
a : α
⊢ (¬∃ᶠ (y : α) in 𝓝 a, ∃ᶠ (x : α) in 𝓝 y, p x) ↔ ¬∃ᶠ (x : α) in 𝓝 a, p x
[PROOFSTEP]
simp only [not_frequently, eventually_eventually_nhds]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
P : Set α → Prop
hP : ∀ (s t : Set α), s ⊆ t → P s → P t
⊢ (∀ (i : Set α), x ∈ i ∧ IsOpen i → P i) ↔ ∀ (s : Set α), IsOpen s → x ∈ s → P s
[PROOFSTEP]
simp only [@and_comm (x ∈ _), and_imp]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
⊢ (∀ (ib : Set α), a ∈ ib ∧ IsOpen ib → ∃ ia, True ∧ ∀ (x : β), x ∈ Ici ia → f x ∈ ib) ↔
    ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : β), N ≤ n → f n ∈ U
[PROOFSTEP]
simp only [and_imp, exists_prop, true_and_iff, mem_Ici, ge_iff_le]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
F : Filter α
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
[PROOFSTEP]
rw [disjoint_iff, ClusterPt, neBot_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
s : Set α
⊢ ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : α) in 𝓝 x, y ∈ s
[PROOFSTEP]
simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
f : Filter α
H : f ≤ 𝓝 x
inst✝ : NeBot f
⊢ ClusterPt x f
[PROOFSTEP]
rwa [ClusterPt, inf_eq_right.mpr H]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
f : Filter α
H : 𝓝 x ≤ f
⊢ ClusterPt x f
[PROOFSTEP]
simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
x : α
F : Filter ι
u : ι → α
⊢ MapClusterPt x F u ↔ ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (a : ι) in F, u a ∈ s
[PROOFSTEP]
simp_rw [MapClusterPt, ClusterPt, inf_neBot_iff_frequently_left, frequently_map]
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
ι : Type u_1
x : α
F : Filter ι
u : ι → α
⊢ (∀ {p : α → Prop}, (∀ᶠ (x : α) in 𝓝 x, p x) → ∃ᶠ (a : ι) in F, p (u a)) ↔
    ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (a : ι) in F, u a ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
⊢ MapClusterPt x F u
[PROOFSTEP]
have :=
  calc
    map (u ∘ φ) p = map u (map φ p) := map_map
    _ ≤ map u F := map_mono h
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this : map (u ∘ φ) p ≤ map u F
⊢ MapClusterPt x F u
[PROOFSTEP]
have : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F := le_inf H this
[GOAL]
α : Type u
β : Type v
ι✝ : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
ι : Type u_1
δ : Type u_2
F : Filter ι
φ : δ → ι
p : Filter δ
x : α
u : ι → α
inst✝ : NeBot p
h : Tendsto φ p F
H : Tendsto (u ∘ φ) p (𝓝 x)
this✝ : map (u ∘ φ) p ≤ map u F
this : map (u ∘ φ) p ≤ 𝓝 x ⊓ map u F
⊢ MapClusterPt x F u
[PROOFSTEP]
exact neBot_of_le this
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
F : Filter α
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
[PROOFSTEP]
rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
C : Set α
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
[PROOFSTEP]
rw [acc_iff_cluster, inf_principal, inter_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
C : Set α
⊢ ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C \ {x}))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
C : Set α
⊢ AccPt x (𝓟 C) ↔ ∀ (U : Set α), U ∈ 𝓝 x → ∃ y, y ∈ U ∩ C ∧ y ≠ x
[PROOFSTEP]
simp [acc_principal_iff_cluster, clusterPt_principal_iff, Set.Nonempty, exists_prop, and_assoc, @and_comm (¬_ = x)]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
C : Set α
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
[PROOFSTEP]
simp [acc_principal_iff_cluster, clusterPt_principal_iff_frequently, and_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ interior s ↔ x ∈ {a | s ∈ 𝓝 a}
[PROOFSTEP]
simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ {a | s ∈ 𝓝 a} = {a | 𝓝 a ≤ 𝓟 s}
[PROOFSTEP]
simp only [le_principal_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
p : α → Prop
⊢ IsOpen {x | ∀ᶠ (y : α) in 𝓝 x, p y}
[PROOFSTEP]
simp only [← interior_setOf_eq, isOpen_interior]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s V : Set α
⊢ s ⊆ interior V ↔ ∀ (x : α), x ∈ s → V ∈ 𝓝 x
[PROOFSTEP]
simp_rw [subset_def, mem_interior_iff_mem_nhds]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ interior s ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
[PROOFSTEP]
rw [interior_eq_nhds]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s ⊆ {a | 𝓝 a ≤ 𝓟 s} ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l
[PROOFSTEP]
simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ IsOpen {a} ↔ 𝓝 a = pure a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ IsOpen {a} → 𝓝 a = pure a
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
h : IsOpen {a}
⊢ 𝓝 a = pure a
[PROOFSTEP]
apply le_antisymm _ (pure_le_nhds a)
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
h : IsOpen {a}
⊢ 𝓝 a ≤ pure a
[PROOFSTEP]
rw [le_pure_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
h : IsOpen {a}
⊢ {a} ∈ 𝓝 a
[PROOFSTEP]
exact h.mem_nhds (mem_singleton a)
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a = pure a → IsOpen {a}
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
h : 𝓝 a = pure a
⊢ IsOpen {a}
[PROOFSTEP]
simp [isOpen_iff_nhds, h]
[GOAL]
α✝ : Type u
β : Type v
ι : Sort w
a✝ : α✝
s s₁ s₂ t : Set α✝
p p₁ p₂ : α✝ → Prop
inst✝¹ : TopologicalSpace α✝
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ IsOpen {a} ↔ 𝓝[{a}ᶜ] a = ⊥
[PROOFSTEP]
rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl, ← le_pure_iff, nhds_neBot.le_pure_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
a : α
⊢ a ∈ closure s ↔ ∃ᶠ (x : α) in 𝓝 a, x ∈ s
[PROOFSTEP]
rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds, closure_eq_compl_interior_compl]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
a : α
⊢ a ∈ (interior sᶜ)ᶜ ↔ ¬a ∈ interior {x | ¬x ∈ s}
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed s ↔ ∀ (x : α), (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
[PROOFSTEP]
rw [← closure_subset_iff_isClosed]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s ⊆ s ↔ ∀ (x : α), (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
[PROOFSTEP]
refine' forall_congr' fun x => _
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
[PROOFSTEP]
rw [mem_closure_iff_frequently]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
⊢ IsClosed {x | ClusterPt x f}
[PROOFSTEP]
simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
⊢ IsClosed (⋂ (i : α → Prop), {x | (¬∀ᶠ (x : α) in 𝓝 x, i x) ∨ ∃ᶠ (x : α) in f, i x})
[PROOFSTEP]
refine' isClosed_iInter fun p => IsClosed.union _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsClosed fun x => (∀ᶠ (x : α) in 𝓝 x, p x) → False
[PROOFSTEP]
apply isClosed_compl_iff.2
[GOAL]
case refine'_2
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsClosed fun x => (∀ᶠ (x : α) in f, ¬(fun x => p x) x) → False
[PROOFSTEP]
apply isClosed_compl_iff.2
[GOAL]
case refine'_1
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets (𝓝 x) {x | (fun x => p x) x}
case refine'_2
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets f {x | (fun x => ¬(fun x => p x) x) x}
[PROOFSTEP]
exacts [isOpen_setOf_eventually_nhds, isOpen_const]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
⊢ Dense {x}ᶜ
[PROOFSTEP]
intro y
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
⊢ y ∈ closure {x}ᶜ
[PROOFSTEP]
rcases eq_or_ne y x with (rfl | hne)
[GOAL]
case inl
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
y : α
inst✝ : NeBot (𝓝[{y}ᶜ] y)
⊢ y ∈ closure {y}ᶜ
[PROOFSTEP]
rwa [mem_closure_iff_nhdsWithin_neBot]
[GOAL]
case inr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
hne : y ≠ x
⊢ y ∈ closure {x}ᶜ
[PROOFSTEP]
exact subset_closure hne
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
a : α
⊢ a ∈ closure s ↔ ∀ (t : Set α), t ∈ 𝓝 a → ∃ y, ↑y ∈ t
[PROOFSTEP]
simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
A : Set α
x : α
⊢ x ∈ closure A ↔ NeBot (comap Subtype.val (𝓝 x))
[PROOFSTEP]
simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
p : ι → Prop
s : ι → Set α
h : HasBasis (𝓝 a) p s
t : Set α
⊢ (∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → Set.Nonempty (s i ∩ t)) ↔ ∀ (i : ι), p i → Set.Nonempty (s i ∩ t)
[PROOFSTEP]
simp only [exists_prop, forall_const]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
p : ι → Prop
s : ι → Set α
h : HasBasis (𝓝 a) p s
t : Set α
⊢ (∀ (i : ι), p i → Set.Nonempty (s i ∩ t)) ↔ ∀ (i : ι), p i → ∃ y, y ∈ t ∧ y ∈ s i
[PROOFSTEP]
simp only [Set.Nonempty, mem_inter_iff, exists_prop, and_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
F : Filter α
a : α
⊢ ClusterPt a F ↔ ∀ (s : Set α), s ∈ F → a ∈ closure s
[PROOFSTEP]
simp_rw [ClusterPt, inf_neBot_iff, mem_closure_iff_nhds]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
F : Filter α
a : α
⊢ (∀ ⦃s : Set α⦄, s ∈ 𝓝 a → ∀ ⦃s' : Set α⦄, s' ∈ F → Set.Nonempty (s ∩ s')) ↔
    ∀ (s : Set α), s ∈ F → ∀ (t : Set α), t ∈ 𝓝 a → Set.Nonempty (t ∩ s)
[PROOFSTEP]
rw [forall₂_swap]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
F : Filter α
a : α
⊢ ClusterPt a F ↔ pure a ≤ Filter.lift' F closure
[PROOFSTEP]
simp_rw [clusterPt_iff_forall_mem_closure, (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id,
  singleton_subset_iff, true_and, exists_const]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
F : Filter α
a : α
⊢ ClusterPt a F ↔ NeBot (Filter.lift' F closure ⊓ pure a)
[PROOFSTEP]
rw [clusterPt_iff_lift'_closure, ← Ultrafilter.coe_pure, inf_comm, Ultrafilter.inf_neBot_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
F : Filter α
a : α
⊢ ClusterPt a (Filter.lift' F closure) ↔ ClusterPt a F
[PROOFSTEP]
simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure α) (monotone_closure α)]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x
[PROOFSTEP]
simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s ⊆ s ↔ ∀ (a : α), ClusterPt a (𝓟 s) → a ∈ s
[PROOFSTEP]
simp only [subset_def, mem_closure_iff_clusterPt]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed s ↔ ∀ (x : α), (∀ (U : Set α), U ∈ 𝓝 x → Set.Nonempty (U ∩ s)) → x ∈ s
[PROOFSTEP]
simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h : IsClosed t
⊢ interior (s ∪ t) ⊆ interior s ∪ t
[PROOFSTEP]
simpa only [union_comm _ t] using h.interior_union_left
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h : IsOpen s
⊢ (closure (s ∩ t))ᶜ ⊆ (s ∩ closure t)ᶜ
[PROOFSTEP]
simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h : IsOpen t
⊢ closure s ∩ t ⊆ closure (s ∩ t)
[PROOFSTEP]
simpa only [inter_comm t] using h.inter_closure
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
hs : Dense s
ht : IsOpen t
⊢ t = t ∩ closure s
[PROOFSTEP]
rw [hs.closure_eq, inter_univ]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : x ∈ closure (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ x ∈ closure s₂
[PROOFSTEP]
rw [mem_closure_iff_nhds_neBot] at *
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
[PROOFSTEP]
rwa [←
  calc
    𝓝 x ⊓ principal (s₁ ∪ s₂) = 𝓝 x ⊓ (principal s₁ ⊔ principal s₂) := by rw [sup_principal]
    _ = 𝓝 x ⊓ principal s₁ ⊔ 𝓝 x ⊓ principal s₂ := inf_sup_left
    _ = ⊥ ⊔ 𝓝 x ⊓ principal s₂ := by rw [inf_principal_eq_bot.mpr h₁]
    _ = 𝓝 x ⊓ principal s₂ := bot_sup_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) = 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂)
[PROOFSTEP]
rw [sup_principal]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s s₁✝ s₂✝ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s₁ s₂ : Set α
x : α
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ = ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂
[PROOFSTEP]
rw [inf_principal_eq_bot.mpr h₁]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
hs : Dense s
ht : Dense t
hso : IsOpen s
x : α
⊢ x ∈ closure (s ∩ closure t)
[PROOFSTEP]
simp [hs.closure_eq, ht.closure_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure s \ closure t = (closure t)ᶜ ∩ closure s
[PROOFSTEP]
simp only [diff_eq, inter_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure ((closure t)ᶜ ∩ s) = closure (s \ closure t)
[PROOFSTEP]
simp only [diff_eq, inter_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 a) ↔ Tendsto f l (𝓝 a)
[PROOFSTEP]
rw [tendsto_iff_comap, tendsto_iff_comap]
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
[PROOFSTEP]
replace h : 𝓟 sᶜ ≤ comap f (𝓝 a)
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
⊢ 𝓟 sᶜ ≤ comap f (𝓝 a)
[PROOFSTEP]
rintro U ⟨t, ht, htU⟩ x hx
[GOAL]
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
⊢ x ∈ U
[PROOFSTEP]
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
[GOAL]
case h.intro.intro
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : ∀ (x : β), ¬x ∈ s → f x = a
U : Set β
t : Set α
ht : t ∈ 𝓝 a
htU : f ⁻¹' t ⊆ U
x : β
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U
[PROOFSTEP]
exact htU this
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 sᶜ ≤ comap f (𝓝 a)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 a) ↔ l ≤ comap f (𝓝 a)
[PROOFSTEP]
refine' ⟨fun h' => _, le_trans inf_le_left⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 sᶜ ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
[PROOFSTEP]
have := sup_le h' h
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 sᶜ ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
[PROOFSTEP]
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff] at this
[GOAL]
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : β → α
l : Filter β
s : Set β
a : α
h : 𝓟 sᶜ ≤ comap f (𝓝 a)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 a)
this : l ≤ comap f (𝓝 a) ∧ 𝓟 sᶜ ≤ comap f (𝓝 a)
⊢ l ≤ comap f (𝓝 a)
[PROOFSTEP]
exact this.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
⊢ Continuous g
[PROOFSTEP]
convert h
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
⊢ g = f
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
h : Continuous f
h' : ∀ (x : α), f x = g x
x✝ : α
⊢ g x✝ = f x✝
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f g : α → β
x : α
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x
[PROOFSTEP]
simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
M₀ : Type u_5
inst✝ : Zero M₀
a : α
f : α → M₀
⊢ f =ᶠ[𝓝 a] 0 ↔ ¬a ∈ closure (Function.support f)
[PROOFSTEP]
rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds, Function.compl_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
M₀ : Type u_5
inst✝ : Zero M₀
a : α
f : α → M₀
⊢ f =ᶠ[𝓝 a] 0 ↔ {x | f x = 0} ∈ 𝓝 a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
x : α
y : β
hg : ContinuousAt g y
hf : ContinuousAt f x
hy : f x = y
⊢ ContinuousAt (g ∘ f) x
[PROOFSTEP]
subst hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
x : α
hf : ContinuousAt f x
hg : ContinuousAt g (f x)
⊢ ContinuousAt (g ∘ f) x
[PROOFSTEP]
exact hg.comp hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ (∀ (x : Set β), IsOpen xᶜ → IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set β), IsClosed s → IsClosed (f ⁻¹' s)
[PROOFSTEP]
simp only [isOpen_compl_iff, preimage_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
⊢ Continuous f ↔ ∀ (x : α) (g : Ultrafilter α), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))
[PROOFSTEP]
simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : Continuous f
t : Set β
⊢ closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
[PROOFSTEP]
rw [← (isClosed_closure.preimage hf).closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : Continuous f
t : Set β
⊢ closure (f ⁻¹' t) ⊆ closure (f ⁻¹' closure t)
[PROOFSTEP]
exact closure_mono (preimage_mono subset_closure)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : Continuous f
⊢ MapsTo f (closure s) (closure t)
[PROOFSTEP]
simp only [MapsTo, mem_closure_iff_clusterPt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : Continuous f
⊢ ∀ ⦃x : α⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
[PROOFSTEP]
exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
h : Continuous f
⊢ closure s ⊆ f ⁻¹' closure (f '' s)
[PROOFSTEP]
rw [← Set.image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
h : Continuous f
⊢ f '' closure s ⊆ closure (f '' s)
[PROOFSTEP]
exact image_closure_subset_closure_image h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f : κ → β
g : β → γ
hf : Surjective f
x : β
⊢ x ∈ closure (range f)
[PROOFSTEP]
simp [hf.range_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f : κ → β
g : β → γ
s : Set α
h : Dense s
⊢ DenseRange Subtype.val
[PROOFSTEP]
simpa only [DenseRange, Subtype.range_coe_subtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f✝ : κ → β
g : β → γ
f : α → β
hf : Continuous f
s : Set α
hs : Dense s
⊢ range f ⊆ closure (f '' s)
[PROOFSTEP]
rw [← image_univ, ← hs.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f✝ : κ → β
g : β → γ
f : α → β
hf : Continuous f
s : Set α
hs : Dense s
⊢ f '' closure s ⊆ closure (f '' s)
[PROOFSTEP]
exact image_closure_subset_closure_image hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f : κ → β
g : β → γ
hf : DenseRange f
s : Set β
hs : IsOpen s
⊢ s ⊆ closure (f '' (f ⁻¹' s))
[PROOFSTEP]
rw [image_preimage_eq_inter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f : κ → β
g : β → γ
hf : DenseRange f
s : Set β
hs : IsOpen s
⊢ s ⊆ closure (s ∩ range f)
[PROOFSTEP]
exact hf.open_subset_closure_inter hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f✝ : κ → β
g✝ g : β → γ
f : κ → β
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ DenseRange (g ∘ f)
[PROOFSTEP]
rw [DenseRange, range_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_5
ι : Type u_6
f✝ : κ → β
g✝ g : β → γ
f : κ → β
hg : DenseRange g
hf : DenseRange f
cg : Continuous g
⊢ Dense (g '' range f)
[PROOFSTEP]
exact hg.dense_image cg hf


[GOAL]
α : Type u
⊢ ∀ (t₁ : Set (Ultrafilter α)),
    t₁ ∈ ultrafilterBasis α →
      ∀ (t₂ : Set (Ultrafilter α)),
        t₂ ∈ ultrafilterBasis α →
          ∀ (x : Ultrafilter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
[GOAL]
case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃, t₃ ∈ ultrafilterBasis α ∧ u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b
[PROOFSTEP]
refine' ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv => ⟨_, _⟩⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s => {u | s ∈ u}) a
[PROOFSTEP]
apply mem_of_superset hv
[GOAL]
case intro.intro.intro.refine'_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ v ∈ (fun s => {u | s ∈ u}) b
[PROOFSTEP]
apply mem_of_superset hv
[GOAL]
case intro.intro.intro.refine'_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ a
[PROOFSTEP]
simp [inter_subset_right a b]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s => {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ b
[PROOFSTEP]
simp [inter_subset_right a b]
[GOAL]
α : Type u
s : Set α
⊢ IsClosed {u | s ∈ u}
[PROOFSTEP]
rw [← isOpen_compl_iff]
[GOAL]
α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ
[PROOFSTEP]
convert ultrafilter_isOpen_basic sᶜ using 1
[GOAL]
case h.e'_3
α : Type u
s : Set α
⊢ {u | s ∈ u}ᶜ = {u | sᶜ ∈ u}
[PROOFSTEP]
ext u
[GOAL]
case h.e'_3.h
α : Type u
s : Set α
u : Ultrafilter α
⊢ u ∈ {u | s ∈ u}ᶜ ↔ u ∈ {u | sᶜ ∈ u}
[PROOFSTEP]
exact Ultrafilter.compl_mem_iff_not_mem.symm
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u
[PROOFSTEP]
rw [eq_comm, ← Ultrafilter.coe_le_coe]
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
[PROOFSTEP]
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
[PROOFSTEP]
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff, mem_setOf_eq]
[GOAL]
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) ↔
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u) →
    ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
[PROOFSTEP]
intro h a ha
[GOAL]
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
a : Set α
ha : a ∈ x
⊢ {v | a ∈ v} ∈ u
[PROOFSTEP]
exact h _ ⟨ha, a, rfl⟩
[GOAL]
case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u) →
    ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s => {u | s ∈ u}) → i ∈ ↑u
[PROOFSTEP]
rintro h a ⟨xi, a, rfl⟩
[GOAL]
case mpr.intro.intro
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ (s : Set α), s ∈ x → {v | s ∈ v} ∈ u
a : Set α
xi : x ∈ (fun s => {u | s ∈ u}) a
⊢ (fun s => {u | s ∈ u}) a ∈ ↑u
[PROOFSTEP]
exact h _ xi
[GOAL]
α : Type u
⊢ TotallyDisconnectedSpace (Ultrafilter α)
[PROOFSTEP]
rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
[GOAL]
α : Type u
⊢ ∀ (x : Ultrafilter α), connectedComponent x = {x}
[PROOFSTEP]
intro A
[GOAL]
α : Type u
A : Ultrafilter α
⊢ connectedComponent A = {A}
[PROOFSTEP]
simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and_iff]
[GOAL]
α : Type u
A : Ultrafilter α
⊢ ∀ (x : Ultrafilter α), x ∈ connectedComponent A → x = A
[PROOFSTEP]
intro B hB
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ B = A
[PROOFSTEP]
rw [← Ultrafilter.coe_le_coe]
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
[PROOFSTEP]
rw [connectedComponent_eq_iInter_clopen, Set.mem_iInter] at hB
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
[PROOFSTEP]
let Z := {F : Ultrafilter α | s ∈ F}
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
⊢ s ∈ ↑B
[PROOFSTEP]
have hZ : IsClopen Z := ⟨ultrafilter_isOpen_basic s, ultrafilter_isClosed_basic s⟩
[GOAL]
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { Z // IsClopen Z ∧ A ∈ Z }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
hZ : IsClopen Z
⊢ s ∈ ↑B
[PROOFSTEP]
exact hB ⟨Z, hZ, hs⟩
[GOAL]
α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)
[PROOFSTEP]
rw [Tendsto, ← coe_map, ultrafilter_converges_iff]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ s ∈ joinM (map pure b)
[PROOFSTEP]
change s ∈ b ↔ {t | s ∈ t} ∈ map pure b
[GOAL]
case h
α : Type u
b : Ultrafilter α
s : Set α
⊢ s ∈ b ↔ {t | s ∈ t} ∈ map pure b
[PROOFSTEP]
simp_rw [mem_map, preimage_setOf_eq, mem_pure, setOf_mem_eq]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b
[PROOFSTEP]
rw [TopologicalSpace.nhds_generateFrom]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ (s : Set (Ultrafilter α)) (_ : s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 s) ≤ ↑b
[PROOFSTEP]
simp only [comap_iInf, comap_principal]
[GOAL]
α : Type u
b : Ultrafilter α
⊢ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i) ≤ ↑b
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i)
[PROOFSTEP]
rw [← le_principal_iff]
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (i : Set (Ultrafilter α)) (_ : i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' i) ≤ 𝓟 s
[PROOFSTEP]
refine' iInf_le_of_le {u | s ∈ u} _
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ (_ : {u | s ∈ u} ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}), 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
[PROOFSTEP]
refine' iInf_le_of_le ⟨hs, ⟨s, rfl⟩⟩ _
[GOAL]
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ 𝓟 (pure ⁻¹' {u | s ∈ u}) ≤ 𝓟 s
[PROOFSTEP]
exact principal_mono.2 fun a => id
[GOAL]
α : Type u
⊢ Function.Injective pure
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u
x y : α
h : pure x = pure y
⊢ x = y
[PROOFSTEP]
have : { x } ∈ (pure x : Ultrafilter α) := singleton_mem_pure
[GOAL]
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure x
⊢ x = y
[PROOFSTEP]
rw [h] at this
[GOAL]
α : Type u
x y : α
h : pure x = pure y
this : {x} ∈ pure y
⊢ x = y
[PROOFSTEP]
exact (mem_singleton_iff.mp (mem_pure.mp this)).symm
[GOAL]
α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥
[PROOFSTEP]
apply eq_bot_of_singletons_open
[GOAL]
case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}
[PROOFSTEP]
intro x
[GOAL]
case h
α : Type u
x : α
⊢ IsOpen {x}
[PROOFSTEP]
use{u : Ultrafilter α | { x } ∈ u}, ultrafilter_isOpen_basic _
[GOAL]
case right
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
[PROOFSTEP]
simp
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
letI : TopologicalSpace α := ⊥
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this : TopologicalSpace α := ⊥
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
haveI : DiscreteTopology α := ⟨rfl⟩
[GOAL]
α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
this✝ : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Ultrafilter.extend f ∘ pure = f
[PROOFSTEP]
exact funext (denseInducing_pure.extend_eq continuous_of_discreteTopology)
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
have h : ∀ b : Ultrafilter α, ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c) :=
  fun b =>
    -- b.map f is an ultrafilter on γ, which is compact, so it converges to some c in γ.
  let ⟨c, _, h'⟩ := isCompact_univ.ultrafilter_le_nhds (b.map f) (by rw [le_principal_iff]; exact univ_mem)
  ⟨c, le_trans (map_mono (ultrafilter_comap_pure_nhds _)) h'⟩
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ ↑(Ultrafilter.map f b) ≤ 𝓟 univ
[PROOFSTEP]
rw [le_principal_iff]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)
[PROOFSTEP]
exact univ_mem
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
letI : TopologicalSpace α := ⊥
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
this : TopologicalSpace α := ⊥
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
haveI : NormalSpace γ := normalOfCompactT2
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
this✝ : TopologicalSpace α := ⊥
this : NormalSpace γ
⊢ Continuous (Ultrafilter.extend f)
[PROOFSTEP]
exact denseInducing_pure.continuous_extend h
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
let b' : Ultrafilter (Ultrafilter α) := b.map pure
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
have t : ↑b' ≤ 𝓝 b := ultrafilter_converges_iff.mpr (bind_pure _).symm
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
[PROOFSTEP]
have := (continuous_ultrafilter_extend f).tendsto b
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
[PROOFSTEP]
refine' le_trans _ (le_trans (map_mono t) this)
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f) ↑b'
[PROOFSTEP]
change _ ≤ map (Ultrafilter.extend f ∘ pure) ↑b
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f ∘ pure) ↑b
[PROOFSTEP]
rw [ultrafilter_extend_extends]
[GOAL]
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map f ↑b
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ TopologicalSpace (StoneCech α)
[PROOFSTEP]
unfold StoneCech
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ TopologicalSpace (Quotient (stoneCechSetoid α))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Inhabited α
⊢ Inhabited (StoneCech α)
[PROOFSTEP]
unfold StoneCech
[GOAL]
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Inhabited α
⊢ Inhabited (Quotient (stoneCechSetoid α))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ g₁ = g₂
[PROOFSTEP]
apply Continuous.ext_on denseRange_stoneCechUnit h₁ h₂
[GOAL]
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
⊢ EqOn g₁ g₂ (range stoneCechUnit)
[PROOFSTEP]
rintro x ⟨x, rfl⟩
[GOAL]
case intro
α : Type u
inst✝⁵ : TopologicalSpace α
γ : Type u
inst✝⁴ : TopologicalSpace γ
inst✝³ : T2Space γ
inst✝² : CompactSpace γ
γ' : Type u
inst✝¹ : TopologicalSpace γ'
inst✝ : T2Space γ'
f : α → γ
hf : Continuous f
g₁ g₂ : StoneCech α → γ'
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit
x : α
⊢ g₁ (stoneCechUnit x) = g₂ (stoneCechUnit x)
[PROOFSTEP]
apply congr_fun h x
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
[PROOFSTEP]
skip
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = Ultrafilter.extend f (pure x)
[PROOFSTEP]
trans f x
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
[PROOFSTEP]
swap
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ f x = Ultrafilter.extend f (pure x)
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
all_goals refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f (pure x) = f x
[PROOFSTEP]
refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f u = f x
[PROOFSTEP]
refine' ultrafilter_extend_eq_iff.mpr (le_trans (map_mono _) (hf.tendsto _))
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑(pure x) ≤ 𝓝 x
[PROOFSTEP]
apply pure_le_nhds
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
u : Ultrafilter α
x : α
ux : ↑u ≤ 𝓝 x
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ ↑u ≤ 𝓝 x
[PROOFSTEP]
exact ux
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
have : (g.map pure).toFilter ≤ 𝓝 g := by
  rw [ultrafilter_converges_iff]
  exact (bind_pure _).symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g
[PROOFSTEP]
rw [ultrafilter_converges_iff]
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g = joinM (Ultrafilter.map pure g)
[PROOFSTEP]
exact (bind_pure _).symm
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
have : (g.map stoneCechUnit : Filter (StoneCech α)) ≤ 𝓝 ⟦g⟧ :=
  continuousAt_iff_ultrafilter.mp (continuous_quotient_mk'.tendsto g) _ this
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : ↑(Ultrafilter.map stoneCechUnit g) ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) g)
⊢ Tendsto stoneCechUnit (↑g) (𝓝 (stoneCechUnit x))
[PROOFSTEP]
rwa [show ⟦g⟧ = ⟦pure x⟧ from Quotient.sound <| convergent_eqv_pure gx] at this
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ T2Space (StoneCech α)
[PROOFSTEP]
rw [t2_iff_ultrafilter]
[GOAL]
α : Type u
inst✝ : TopologicalSpace α
⊢ ∀ {x y : StoneCech α} (f : Ultrafilter (StoneCech α)), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩ g gx gy
[GOAL]
case mk.mk
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
⊢ Quot.mk Setoid.r x = Quot.mk Setoid.r y
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
⊢ x ≈ y
[PROOFSTEP]
intro γ tγ h₁ h₂ f hf
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
skip
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
let ff := stoneCechExtend hf
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
⊢ Ultrafilter.extend f x = Ultrafilter.extend f y
[PROOFSTEP]
change ff ⟦x⟧ = ff ⟦y⟧
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
⊢ ff (Quotient.mk (stoneCechSetoid α) x) = ff (Quotient.mk (stoneCechSetoid α) y)
[PROOFSTEP]
have lim := fun (z : Ultrafilter α) (gz : (g : Filter (StoneCech α)) ≤ 𝓝 ⟦z⟧) =>
  ((continuous_stoneCechExtend hf).tendsto _).mono_left gz
[GOAL]
case mk.mk.a
α : Type u
inst✝ : TopologicalSpace α
x✝ : StoneCech α
x : Ultrafilter α
y✝ : StoneCech α
y : Ultrafilter α
g : Ultrafilter (StoneCech α)
gx : ↑g ≤ 𝓝 (Quot.mk Setoid.r x)
gy : ↑g ≤ 𝓝 (Quot.mk Setoid.r y)
γ : Type u
tγ : TopologicalSpace γ
h₁ : T2Space γ
h₂ : CompactSpace γ
f : α → γ
hf : Continuous f
ff : StoneCech α → γ := stoneCechExtend hf
lim :
  ∀ (z : Ultrafilter α),
    ↑g ≤ 𝓝 (Quotient.mk (stoneCechSetoid α) z) →
      Tendsto (stoneCechExtend hf) (↑g) (𝓝 (stoneCechExtend hf (Quotient.mk (stoneCechSetoid α) z)))
⊢ ff (Quotient.mk (stoneCechSetoid α) x) = ff (Quotient.mk (stoneCechSetoid α) y)
[PROOFSTEP]
exact tendsto_nhds_unique (lim x gx) (lim y gy)