infinite_of_nontrivial — Mathlib

English

If s is a preconnected subset of X and s is nontrivial, then s is infinite (in a T1 space).

Русский

Если s — предсоединённое подмножество X и оно не тривиально, то оно бесконечно во времени (в T1-пространстве).

LaTeX

$$$IsPreconnected(s) \rightarrow s.Nontrivial \rightarrow s.Infinite$$$

Lean4

theorem infinite_of_nontrivial [T1Space X] {s : Set X} (h : IsPreconnected s) (hs : s.Nontrivial) : s.Infinite :=
  by
  refine mt (fun hf => (subsingleton_coe s).mp ?_) (not_subsingleton_iff.mpr hs)
  haveI := @Finite.instDiscreteTopology s _ _ hf.to_subtype
  exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _

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