trivial_of_discrete — Mathlib

English

If X is a PreconnectedSpace with the discrete topology, then X is a singleton.

Русский

Если X — предсоединённое пространство с дискретной топологией, то X однопунктно.

LaTeX

$$$[\text{PreconnectedSpace } X] \land [\text{DiscreteTopology } X] \Rightarrow \text{Subsingleton}(X)$$$

Lean4

theorem trivial_of_discrete [PreconnectedSpace X] [DiscreteTopology X] : Subsingleton X :=
  by
  by_contra! h
  rcases h with ⟨x, y, hxy⟩
  rw [Ne, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy
  exact hxy (mem_univ x)

Похожие утверждения