English
If two functions u and v are each bounded above along a filter f, then the pointwise supremum a ↦ u(a) ⊔ v(a) is also bounded above along f. Moreover, the bound can be taken as bu ⊔ bv if bu bounds u and bv bounds v.
Русский
Если две функции u и v ограничены сверху вдоль фильтра f, то функция a ↦ u(a) ⊔ v(a) тоже ограничена сверху вдоль f. Граница может быть взята как bu ⊔ bv, если bu и bv являются верхними границами для u и v соответственно.
LaTeX
$$$\bigl(\operatorname{IsBoundedUnder}(\le, l)(u)\bigr) \rightarrow\bigl(\operatorname{IsBoundedUnder}(\le, l)(v)\bigr) \rightarrow \operatorname{IsBoundedUnder}(\le, l)(\lambda a. u(a) \sqcup v(a))$$$
Lean4
theorem sup [SemilatticeSup α] {f : Filter β} {u v : β → α} :
f.IsBoundedUnder (· ≤ ·) u → f.IsBoundedUnder (· ≤ ·) v → f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a
| ⟨bu, (hu : ∀ᶠ x in f, u x ≤ bu)⟩, ⟨bv, (hv : ∀ᶠ x in f, v x ≤ bv)⟩ =>
⟨bu ⊔ bv, show ∀ᶠ x in f, u x ⊔ v x ≤ bu ⊔ bv by filter_upwards [hu, hv] with _ using sup_le_sup⟩
