α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
⊢ ¬Nontrivial α
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
⊢ Subsingleton α
rw [← not_nontrivial_iff_subsingleton]
case mk.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
x y : α
hxy : x ≠ y
⊢ False
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
⊢ ¬Nontrivial α
rintro ⟨x, y, hxy⟩
case mk.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
x y : α
hxy : ¬x ∈ univ
⊢ False
case mk.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
x y : α
hxy : x ≠ y
⊢ False
rw [Ne.def, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy
no goals
case mk.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
inst✝ : DiscreteTopology α
x y : α
hxy : ¬x ∈ univ
⊢ False
exact hxy (mem_univ x)