α : Type u
β : Type v
ι : Type ?u.204087
π : ι → Type ?u.204092
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U : Set α
hS : IsPreirreducible S
hU : IsOpen U
h : Set.Nonempty (S ∩ U)
h' : ¬S ⊆ closure (S ∩ U)
⊢ False
α : Type u
β : Type v
ι : Type ?u.204087
π : ι → Type ?u.204092
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U : Set α
hS : IsPreirreducible S
hU : IsOpen U
h : Set.Nonempty (S ∩ U)
⊢ S ⊆ closure (S ∩ U)
by_contra h'
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204087
π : ι → Type ?u.204092
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U : Set α
hS : IsPreirreducible S
hU : IsOpen U
h : Set.Nonempty (S ∩ U)
h' : ¬S ⊆ closure (S ∩ U)
x : α
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ closure (S ∩ U)ᶜ
⊢ False
α : Type u
β : Type v
ι : Type ?u.204087
π : ι → Type ?u.204092
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U : Set α
hS : IsPreirreducible S
hU : IsOpen U
h : Set.Nonempty (S ∩ U)
h' : ¬S ⊆ closure (S ∩ U)
⊢ False
obtain ⟨x, h₁, h₂, h₃⟩ :=
  hS _ (closure (S ∩ U)ᶜ) hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')
no goals
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.204087
π : ι → Type ?u.204092
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t S U : Set α
hS : IsPreirreducible S
hU : IsOpen U
h : Set.Nonempty (S ∩ U)
h' : ¬S ⊆ closure (S ∩ U)
x : α
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ closure (S ∩ U)ᶜ
⊢ False
exact h₃ (subset_closure ⟨h₁, h₂⟩)