inf — Mathlib

English

If f =^l f' and g =^l g' then f ⊓ g =^l f' ⊓ g'.

Русский

Если 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') \\\\land \\\\ (g =^l g') \\\\Rightarrow \\\\bigl(f ⊓ g =^l f' ⊓ g'\\\\bigr)$$$

Lean4

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

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