irreducibleComponent — Mathlib

English

The function x ↦ irreducibleComponent(x) assigns to each x a maximal irreducible subset of X containing x.

Русский

Функция x ↦ irreducibleComponent(x) ассоциирует каждому x максимальное неразложимое множество, содержащее x.

LaTeX

$$$\\operatorname{irreducibleComponent}: X \\to \\mathcal{P}(X) \\quad \\text{(a maximal irreducible subset containing } x\\text{)}$$$

Lean4

/-- A maximal irreducible set that contains a given point. -/
@[stacks 004W "(4)"]
def irreducibleComponent (x : X) : Set X :=
  Classical.choose (exists_preirreducible { x } isPreirreducible_singleton)

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