exists_infIrred_decomposition — Mathlib

English

In a well-founded lattice, every element is the supremum of finitely many sup-irreducible elements.

Русский

В хорошо основанной решетке каждый элемент является верхушкой конечного множества суп-неразложимых элементов.

LaTeX

$$exists_supIrred_decomposition\ (a : α) : ∃ s : Finset α, s.sup id = a ∧ ∀ ⦃b⦄, Finset.instMembership.mem s b → SupIrred b$$

Lean4

/-- In a cowell-founded lattice, any element is the infimum of finitely many inf-irreducible
elements. This is the order-theoretic analogue of prime factorisation. -/
theorem exists_infIrred_decomposition (a : α) : ∃ s : Finset α, s.inf id = a ∧ ∀ ⦃b⦄, b ∈ s → InfIrred b :=
  exists_supIrred_decomposition (α := αᵒᵈ) _

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