English
For a semilatticeInf α, if u and v are each bounded above along a filter f, then their pointwise infimum a ↦ u(a) ⊓ v(a) is also bounded above along f.
Русский
Для полупорядоченного множества сInf, если u и v ограничены сверху вдоль фильтра f, то их точечный инфимум a ↦ u(a) ⊓ v(a) тоже ограничен сверху вдоль f.
LaTeX
$$$\operatorname{IsBoundedUnder}(\ge, l)(u) \land \operatorname{IsBoundedUnder}(\ge, l)(v) \Rightarrow \operatorname{IsBoundedUnder}(\ge, l)(\lambda a. u(a) \inf v(a))$$$
Lean4
theorem inf [SemilatticeInf α] {f : Filter β} {u v : β → α} :
f.IsBoundedUnder (· ≥ ·) u → f.IsBoundedUnder (· ≥ ·) v → f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a :=
IsBoundedUnder.sup (α := αᵒᵈ)
