Theorem: isClosed_closed_inter (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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ IsClosed (s ∩ u)
Tactic:
rw [←closure_subset_iff_isClosed, ←diff_eq_empty]
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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ closure (s ∩ u) \ (s ∩ u) = ∅

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
⊢ closure (s ∩ u) \ (s ∩ u) = ∅
Tactic:
by_contra h
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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : ¬closure (s ∩ u) \ (s ∩ u) = ∅
⊢ False

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : ¬closure (s ∩ u) \ (s ∩ u) = ∅
⊢ False
Tactic:
simp only [← ne_eq, ← nonempty_iff_ne_empty] at h
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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : (closure (s ∩ u) \ (s ∩ u)).Nonempty
⊢ False

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
h : (closure (s ∩ u) \ (s ∩ u)).Nonempty
⊢ False
Tactic:
rcases h with ⟨x, h⟩
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) \ (s ∩ u)
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) \ (s ∩ u)
⊢ False
Tactic:
simp only [mem_diff, mem_inter_iff, not_and] at h
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ False
Tactic:
have sus : closure (s ∩ u) ⊆ s := by
  nth_rw 2 [← sc.closure_eq]; apply closure_mono; apply inter_subset_left
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
⊢ False
Tactic:
have xs := sus h.1
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
⊢ False
Tactic:
have m := not_or.mpr ⟨h.2 xs, not_mem_of_mem_compl (closure_inter_subset_compl vo d h.1)⟩
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : ¬(x ∈ u ∨ x ∈ v)
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : ¬(x ∈ u ∨ x ∈ v)
⊢ False
Tactic:
rw [← mem_union _ _ _] at m
State after:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : x ∉ u ∪ v
⊢ False

State before:
case intro
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s u v : Set X
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
sus : closure (s ∩ u) ⊆ s
xs : x ∈ s
m : x ∉ u ∪ v
⊢ False
Tactic:
exact not_mem_subset suv m xs
State after:
no goals

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ s
Tactic:
nth_rw 2 [← sc.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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ closure s

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ closure (s ∩ u) ⊆ closure s
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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ s ∩ u ⊆ s

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
sc : IsClosed s
vo : IsOpen v
d : Disjoint u v
suv : s ⊆ u ∪ v
x : X
h : x ∈ closure (s ∩ u) ∧ (x ∈ s → x ∉ u)
⊢ s ∩ u ⊆ s
Tactic:
apply inter_subset_left
State after:
no goals