Theorems · Theorem · order theory

exists_sSupIndep_of_sSup_atoms

∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (b : α),
  sSup {a | a ≤ b ∧ IsAtom a} = b → ∃ s, sSupIndep s ∧ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Defined in

Mathlib.Order.CompactlyGenerated.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLatticeIsModularLatticeIsCompactlyGenerated