isIrreducible_iff_singleton — Mathlib

English

In a Hausdorff space, a subset is irreducible if and only if it is a singleton.

Русский

В хаусдорфовом пространстве подмножество ирредуцируемо тогда, когда оно единичное (содержит ровно один элемент).

LaTeX

$$$\\text{IsIrreducible}(S) \\iff \\exists x, S = \\{x\\}$ in a Hausdorff space.$$

Lean4

theorem isIrreducible_iff_singleton [T2Space X] {S : Set X} : IsIrreducible S ↔ ∃ x, S = { x } := by
  rw [IsIrreducible, isPreirreducible_iff_subsingleton, exists_eq_singleton_iff_nonempty_subsingleton]

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