English
Let γ be a semilattice with infimum. If b is the greatest lower bound of a set s, then the greatest lower bound of s together with an added element a is a ⊓ b.
Русский
Пусть γ — полупорядочение с наибольшей нижней границей. Если b является наибольшей нижней границей множества s, то наибольшая нижняя граница множества s вместе с добавлением элемента a равна a ⊓ b.
LaTeX
$$$IsGLB(s, b) \\rightarrow IsGLB(s \\cup \\{a\\}, a \\sqcap b)$$$
Lean4
protected theorem insert [SemilatticeInf γ] (a) {b} {s : Set γ} (hs : IsGLB s b) : IsGLB (insert a s) (a ⊓ b) :=
by
rw [insert_eq]
exact isGLB_singleton.union hs
