Theorems · Theorem · order theory

exists_supIrred_decomposition

∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [WellFoundedLT α] (a : α),
  ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

In a well-founded lattice, any element is the supremum of finitely many sup-irreducible elements. This is the order-theoretic analogue of prime factorisation.

Defined in

Mathlib.Order.Irreducible

Cited by

1 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemilatticeSupOrderBotWellFoundedLT