sup — Mathlib

English

If f =^l f' and g =^l g' then f ⊔ g =^l f' ⊔ g' (Max structure).

Русский

Если f =^l f' и g =^l g', то f ⊔ g =^l f' ⊔ g' (макс-структура).

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall f,f' , g,g' : \\\\alpha \\\\to β, \\\\ (f =^l f') \\\\Rightarrow \\\\ (g =^l g') \\\\Rightarrow \\\\bigl(f ⊔ g =^l f' ⊔ g'\\\\bigr)$$$

Lean4

@[gcongr]
theorem sup [Max β] {l : Filter α} {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f ⊔ g =ᶠ[l] f' ⊔ g' :=
  hf.comp₂ (· ⊔ ·) hg

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