irreducibleComponents — Mathlib

English

The set irreducibleComponents(X) consists of all maximal irreducible subsets of X.

Русский

Множество irreducibleComponents(X) состоит из всех максимальных по включению неразложимых подмножества X.

LaTeX

$$$\\operatorname{irreducibleComponents}(X) = \\{ s \\mid \\operatorname{Maximal}(\\operatorname{IsIrreducible})\\, s\\}$$$

Lean4

/-- The set of irreducible components of a topological space. -/
@[stacks 004V "(2)"]
def irreducibleComponents (X : Type*) [TopologicalSpace X] : Set (Set X) :=
  {s | Maximal IsIrreducible s}

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