α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
⊢ x = y
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
⊢ IsPreirreducible S ↔ Set.Subsingleton S
refine' ⟨fun h x hx y hy => _, Set.Subsingleton.isPreirreducible⟩
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
e : ¬x = y
⊢ False
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
⊢ x = y
by_contra e
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
e : ¬x = y
U V : Set α
hU : IsOpen U
hV : IsOpen V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
e : ¬x = y
⊢ False
obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := t2_separation e
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.142380
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
S : Set α
h : IsPreirreducible S
x : α
hx : x ∈ S
y : α
hy : y ∈ S
e : ¬x = y
U V : Set α
hU : IsOpen U
hV : IsOpen V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False
exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono <| inter_subset_right _ _).not_disjoint h'