irreducibleSpace_def — Mathlib

English

A space X is irreducible as a space iff the whole space considered as a subset is irreducible.

Русский

Пространство X неразложимо по отношению к самому себе как множеству, аналогично термину irreducibleSpace.

LaTeX

$$$\\text{IrreducibleSpace}(X) \\iff \\operatorname{IsIrreducible}(\\top : Set X)$$$

Lean4

theorem irreducibleSpace_def (X : Type*) [TopologicalSpace X] : IrreducibleSpace X ↔ IsIrreducible (⊤ : Set X) :=
  ⟨@IrreducibleSpace.isIrreducible_univ X _, fun h =>
    haveI : PreirreducibleSpace X := ⟨h.2⟩
    ⟨⟨h.1.some⟩⟩⟩

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