exists_sSupIndep_of_sSup_atoms — Mathlib

English

Given b and h: sSup of atoms below b equals b, there exists a set s of atoms with sSupIndep s, sSup s = b, and every a ∈ s is an atom.

Русский

Пусть b и h удовлетворяют: sSup атомов ниже b равно b; тогда существует множество атомов s such that sSupIndep s, sSup s = b, и каждый элемент — атом.

LaTeX

$$$ \forall b, \big(\, sSup\{a : α \mid IsAtom a, a \le b\} = b \rightarrow \exists s, sSupIndep s \land sSup s = b \land \forall a \in s, IsAtom a \) $$$

Lean4

theorem exists_sSupIndep_of_sSup_atoms (b : α) (h : sSup ({a ≤ b | IsAtom a}) = b) :
    ∃ s : Set α, sSupIndep s ∧ sSup s = b ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
  let ⟨s, s_ind, _, s_atoms⟩ := exists_sSupIndep_disjoint_sSup_atoms ⊥ b bot_le h
  ⟨s, s_ind, by simpa using s_atoms⟩

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