exists_sSupIndep_isCompl_sSup_atoms

English

Equivalently, a ∧ sSup s equals the iSup over Finsets t of a ∧ (t.sup id), under the appropriate order assumptions.

Русский

Эквивалентно: a ∧ sSup s = ⨆ t Finset α, ⦗t ⊆ s⦘ a ∧ t.sup id.

LaTeX

$$$ a \wedge \operatorname{sSup} s = \bigsqcup_{t \subseteq s} (a \wedge t.sup\ id) $$$

Lean4

/-- In an atomic lattice, every element `b` has a complement of the form `sSup s`, where each
element of `s` is an atom. See also `complementedLattice_of_sSup_atoms_eq_top`. -/
theorem exists_sSupIndep_isCompl_sSup_atoms (h : sSup {a : α | IsAtom a} = ⊤) (b : α) :
    ∃ s : Set α, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a := by
  simpa [isCompl_iff, codisjoint_iff, and_assoc] using
    exists_sSupIndep_disjoint_sSup_atoms b ⊤ le_top <| by simpa using h

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