isIrreducible_univ — Mathlib

English

If X is an irreducible space, then the whole space X is irreducible: IsIrreducible(univ).

Русский

Если X — неразложимое пространство, то все пространство неразложимо: IsIrreducible(univ).

LaTeX

$$$\\text{In an irreducible space } IsIrreducible(X) \\text{ with } univ.$$$

Lean4

theorem isIrreducible_univ (X : Type*) [TopologicalSpace X] [IrreducibleSpace X] : IsIrreducible (univ : Set X) :=
  ⟨univ_nonempty, PreirreducibleSpace.isPreirreducible_univ⟩

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