English
For x ∈ X, irreducibleComponent(x) is irreducible, contains {x}, and is maximal among irreducible sets containing x.
Русский
Для x ∈ X irreducibleComponent(x) неразложимо, содержит {x} и максимальна среди всех неразложимых множеств, содержащих x.
LaTeX
$$$\\operatorname{IsPreirreducible}(\\operatorname{irreducibleComponent}(x)) \\land \\{x\\} \\subseteq \\operatorname{irreducibleComponent}(x) \\land \\forall u, \\operatorname{IsPreirreducible}(u) \\rightarrow \\operatorname{irreducibleComponent}(x) \\subseteq u \\rightarrow u = \\operatorname{irreducibleComponent}(x)$$$
Lean4
theorem irreducibleComponent_property (x : X) :
IsPreirreducible (irreducibleComponent x) ∧
{ x } ⊆ irreducibleComponent x ∧
∀ u, IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x :=
Classical.choose_spec (exists_preirreducible { x } isPreirreducible_singleton)
