[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
