eq_irreducibleComponent — Mathlib

English

If s is irreducible and irreducibleComponent(x) ⊆ s, then s = irreducibleComponent(x).

Русский

Если s неразложимо и irreducibleComponent(x) ⊆ s, то s = irreducibleComponent(x).

LaTeX

$$$\\operatorname{IsPreirreducible}(s) \\rightarrow \\operatorname{irreducibleComponent}(x) \\subseteq s \\rightarrow s = \\operatorname{irreducibleComponent}(x)$$$

Lean4

theorem eq_irreducibleComponent {x : X} :
    IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x :=
  (irreducibleComponent_property x).2.2 _

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