sup — Mathlib

English

If f1 ≤ᶠ[l] f2 and g1 ≤ᶠ[l] g2, then f1 ⊔ g1 ≤ᶠ[l] f2 ⊔ g2.

Русский

Если f1 ≤ᶠ[l] f2 и g1 ≤ᶠ[l] g2, то f1 ⊔ g1 ≤ᶠ[l] f2 ⊔ g2.

LaTeX

$$$$ f_1 \\leq^{\\!l} f_2 \\quad\\text{and}\\quad g_1 \\leq^{\\!l} g_2 \\Rightarrow f_1 \\sqcup g_1 \\leq^{\\!l} f_2 \\sqcup g_2. $$$$

Lean4

theorem sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
    f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂ := by filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx

Похожие утверждения