English
Not SupIrred a is equivalent to IsMin a or a split into two smaller parts under a join.
Русский
Не SupIrred a эквивалентно тому, что a минимален или его можно разложить на две меньшие части через операцию объединения.
LaTeX
$$¬SupIrred\ a \iff IsMin\ a \lor \exists b \ c, b ⊔ c = a ∧ b < a ∧ c < a$$
Lean4
/-- 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. -/
theorem exists_supIrred_decomposition (a : α) : ∃ s : Finset α, s.sup id = a ∧ ∀ ⦃b⦄, b ∈ s → SupIrred b := by
classical
apply WellFoundedLT.induction a _
clear a
rintro a ih
by_cases ha : SupIrred a
· exact ⟨{ a }, by simp [ha]⟩
rw [not_supIrred] at ha
obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
· exact ⟨∅, by simp [ha.eq_bot]⟩
obtain ⟨s, rfl, hs⟩ := ih _ hb
obtain ⟨t, rfl, ht⟩ := ih _ hc
exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩
