Theorem: isTotallyDisconnected_iff_totally_disconnected_subtype (Ray/Misc/TotallyDisconnected.lean)

State before:
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
Tactic:
constructor
State after:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s → IsTotallyDisconnected s

case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ IsTotallyDisconnected s → TotallyDisconnectedSpace ↑s

State before:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ TotallyDisconnectedSpace ↑s → IsTotallyDisconnected s
Tactic:
intro h
State after:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
⊢ IsTotallyDisconnected s

State before:
case mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
⊢ IsTotallyDisconnected s
Tactic:
by_cases ne : s.Nonempty
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
⊢ IsTotallyDisconnected s

case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : ¬s.Nonempty
⊢ IsTotallyDisconnected s

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
⊢ IsTotallyDisconnected s
Tactic:
intro t ts tc
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
⊢ t.Subsingleton

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
⊢ t.Subsingleton
Tactic:
set t' := ne.invCoe '' t
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
⊢ t.Subsingleton

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
⊢ t.Subsingleton
Tactic:
have tc' : IsPreconnected t' := tc.image _ (ne.continuousOn_invCoe.mono ts)
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
⊢ t.Subsingleton

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
⊢ t.Subsingleton
Tactic:
have q := h.isTotallyDisconnected_univ _ (subset_univ _) tc'
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ t.Subsingleton

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ t.Subsingleton
Tactic:
rw [e]
State after:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ ((fun x => ↑x) '' t').Subsingleton

State before:
case pos
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
e : t = (fun x => ↑x) '' t'
⊢ ((fun x => ↑x) '' t').Subsingleton
Tactic:
exact q.image _
State after:
no goals

State before:
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ t = (fun x => ↑x) '' t'
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ ∀ (x : X), x ∈ t ↔ x ∈ (fun x => ↑x) '' t'

State before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
⊢ ∀ (x : X), x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Tactic:
intro x
State after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ x ∈ (fun x => ↑x) '' t'

State before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ x ∈ (fun x => ↑x) '' t'
Tactic:
simp only [mem_image]
State after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ ∃ x_1 ∈ t', ↑x_1 = x

State before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t ↔ ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
constructor
State after:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t → ∃ x_1 ∈ t', ↑x_1 = x

case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ (∃ x_1 ∈ t', ↑x_1 = x) → x ∈ t

State before:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ x ∈ t → ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
intro xt
State after:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ∃ x_1 ∈ t', ↑x_1 = x

State before:
case h.mp
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ∃ x_1 ∈ t', ↑x_1 = x
Tactic:
use ⟨x, ts xt⟩
State after:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ⟨x, ⋯⟩ ∈ t' ∧ ↑⟨x, ⋯⟩ = x

State before:
case h
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ⟨x, ⋯⟩ ∈ t' ∧ ↑⟨x, ⋯⟩ = x
Tactic:
refine ⟨⟨x,xt,?_⟩,?_⟩
State after:
case h.refine_1
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ne.invCoe x = ⟨x, ⋯⟩

case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x

State before:
case h.refine_1
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ne.invCoe x = ⟨x, ⋯⟩

case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Tactic:
simp only [Subtype.ext_iff, Subtype.coe_mk, ne.right_invCoe _ (ts xt)]
State after:
case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x

State before:
case h.refine_2
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
xt : x ∈ t
⊢ ↑⟨x, ⋯⟩ = x
Tactic:
rw [Subtype.coe_mk]
State after:
no goals

State before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x : X
⊢ (∃ x_1 ∈ t', ↑x_1 = x) → x ∈ t
Tactic:
intro ⟨⟨y, ys⟩, ⟨z, zt, zy⟩, yx⟩
State after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
zy : ne.invCoe z = ⟨y, ys⟩
yx : ↑⟨y, ys⟩ = x
⊢ x ∈ t

State before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
zy : ne.invCoe z = ⟨y, ys⟩
yx : ↑⟨y, ys⟩ = x
⊢ x ∈ t
Tactic:
simp only [Subtype.coe_mk, Subtype.ext_iff, ne.right_invCoe _ (ts zt)] at yx zy
State after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ x ∈ t

State before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ x ∈ t
Tactic:
rw [← yx, ← zy]
State after:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ z ∈ t

State before:
case h.mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s.Nonempty
t : Set X
ts : t ⊆ s
tc : IsPreconnected t
t' : Set ↑s := ne.invCoe '' t
tc' : IsPreconnected t'
q : t'.Subsingleton
x y : X
ys : y ∈ s
z : X
zt : z ∈ t
yx : y = x
zy : z = y
⊢ z ∈ t
Tactic:
exact zt
State after:
no goals

State before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : ¬s.Nonempty
⊢ IsTotallyDisconnected s
Tactic:
simp only [not_nonempty_iff_eq_empty] at ne
State after:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected s

State before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected s
Tactic:
rw [ne]
State after:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected ∅

State before:
case neg
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : TotallyDisconnectedSpace ↑s
ne : s = ∅
⊢ IsTotallyDisconnected ∅
Tactic:
exact isTotallyDisconnected_empty
State after:
no goals

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
⊢ IsTotallyDisconnected s → TotallyDisconnectedSpace ↑s
Tactic:
intro h
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace ↑s

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace ↑s
Tactic:
refine ⟨?_⟩
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected univ

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected univ
Tactic:
apply embedding_subtype_val.isTotallyDisconnected
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected (Subtype.val '' univ)

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected (Subtype.val '' univ)
Tactic:
rw [Subtype.coe_image_univ]
State after:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected s

State before:
case mpr
X : Type
inst✝ : TopologicalSpace X
s : Set X
h : IsTotallyDisconnected s
⊢ IsTotallyDisconnected s
Tactic:
exact h
State after:
no goals