sup_le — Mathlib

English

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

Русский

Если f1 ≤ᶠ[l] h и g1 ≤ᶠ[l] h, тогда f1 ⊔ g1 ≤ᶠ[l] h.

LaTeX

$$$$ l.EventuallyLE f_1 h \\to l.EventuallyLE g_1 h \\to l.EventuallyLE (\\max f_1 g_1) h $$$$

Lean4

theorem sup_le [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h := by
  filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx

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