English
Let f be a filter and u, v : β → α with α a semilattice where sup exists. Then f is bounded above for the function a ↦ u(a) ⊔ v(a) if and only if f is bounded above for both u and for v separately.
Русский
Пусть фильтр f и функции u, v : β → α, где α — полупорядочное множество с верхней границей (существует sup). Тогда f ограничено сверху по функции a ↦ u(a) ⊔ v(a) тогда и только тогда, когда f ограничено сверху по u и по v по отдельности.
LaTeX
$$$\operatorname{IsBoundedUnder}(\le, f)(u \sqcup v) \iff \left(\operatorname{IsBoundedUnder}(\le, f)u \land \operatorname{IsBoundedUnder}(\le, f)v\right)$$$
Lean4
@[simp]
theorem isBoundedUnder_le_sup [SemilatticeSup α] {f : Filter β} {u v : β → α} :
(f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a) ↔ f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≤ ·) v :=
⟨fun h =>
⟨h.mono_le <| Eventually.of_forall fun _ => le_sup_left, h.mono_le <| Eventually.of_forall fun _ => le_sup_right⟩,
fun h => h.1.sup h.2⟩
