English
Let α be a semilattice with inf. For any subset s of α and any element a ∈ α, the greatest lower bound of a with infClosure(s) equals the greatest lower bound of a with s; i.e., IsGLB(infClosure(s), a) if and only if IsGLB(s, a).
Русский
Пусть α — полугруппа порядков по операции meet (inf). Для произвольного множества s ⊆ α и любого элемента a ∈ α наибольшая нижняя грань a совместно с infClosure(s) совпадает с наибольшей нижней гранью a совместно с s; то есть IsGLB(infClosure(s), a) эквивалентно IsGLB(s, a).
LaTeX
$$$\mathrm{IsGLB}(\infClosure s, a) \iff \mathrm{IsGLB}(s, a)$$$
Lean4
@[simp]
theorem isGLB_infClosure : IsGLB (infClosure s) a ↔ IsGLB s a := by simp [IsGLB]
