instPreirreducibleSpaceOfSubsingleton

English

If X is a subsingleton, then X with the trivial topology is preirreducible.

Русский

Если X является подмножество из одного элемента, то с тривиальной топологией пространство X является преднеразложимым.

LaTeX

$$$[\text{Subsingleton } X] \Rightarrow \mathrm{PreirreducibleSpace}(X)$$$

Lean4

instance (priority := low) [Subsingleton X] : PreirreducibleSpace X :=
  ⟨(Set.subsingleton_univ_iff.mpr ‹_›).isPreirreducible⟩

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