α : Type u_1
β : Type ?u.3096
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
α : Type u_1
β : Type ?u.3096
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
no goals
α : Type u_1
β : Type ?u.3096
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x y : α
S U Z : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and_iff, closure, subset_sInter_iff,
  mem_setOf_eq, and_imp, singleton_subset_iff]