Theorem: closure_inter_subset_compl (Ray/Misc/Connected.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ vᶜ
Tactic:
rw [← vo.isClosed_compl.closure_eq]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ closure vᶜ

State before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ closure (s ∩ u) ⊆ closure vᶜ
Tactic:
apply closure_mono
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ s ∩ u ⊆ vᶜ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
vo : IsOpen v
d : Disjoint u v
⊢ s ∩ u ⊆ vᶜ
Tactic:
exact _root_.trans (inter_subset_right _ _) (Disjoint.subset_compl_left d.symm)
State after:
no goals