isLUB_atoms_le — Mathlib

English

For an atomistic poset with a bottom, the atoms below b have b as their least upper bound.

Русский

Для атомистического частичного порядка с нулем нижних атомов под b существует наименьшая верхняя граница, равная b.

LaTeX

$$$IsLUB\\{a : \\alpha \\mid IsAtom a \\land a \\le b\\} \\; b$$$

Lean4

theorem isLUB_atoms_le (b : α) : IsLUB {a : α | IsAtom a ∧ a ≤ b} b :=
  by
  rcases isLUB_atoms b with ⟨s, hsb, hs⟩
  exact ⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩

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