exists_mem_irreducibleComponents_subset_of_isIrreducible

English

For any irreducible s, there exists an irreducible component u containing s.

Русский

Для любого неразложимого s существует компонента irreducible u, содержащая s.

LaTeX

$$$\\forall s, \\operatorname{IsIrreducible}(s) \\rightarrow \\exists u \\in \\operatorname{irreducibleComponents}(X), s \\subseteq u$$$

Lean4

@[stacks 004W "(3)"]
theorem exists_mem_irreducibleComponents_subset_of_isIrreducible (s : Set X) (hs : IsIrreducible s) :
    ∃ u ∈ irreducibleComponents X, s ⊆ u :=
  by
  obtain ⟨u, hu⟩ := exists_preirreducible s hs.isPreirreducible
  use u, ⟨⟨hs.left.mono hu.right.left, hu.left⟩, fun _ h hl => (hu.right.right _ h.right hl).le⟩
  exact hu.right.left

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