insert — Mathlib

English

In a semilattice with join, if s has lub b, then inserting a yields lub a ⊔ b.

Русский

В полупорядоченном множестве с объединением, если у множества s есть верхняя граница b, то вставка элемента даёт верхнюю границу a ⊔ b.

LaTeX

$$$\\text{IsLUB}(s, b) \\rightarrow \\text{IsLUB}(\\mathrm{insert}\\ a\\ s, a \\oplus b)$$$

Lean4

protected theorem insert [SemilatticeSup γ] (a) {b} {s : Set γ} (hs : IsLUB s b) : IsLUB (insert a s) (a ⊔ b) :=
  by
  rw [insert_eq]
  exact isLUB_singleton.union hs

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