mul — Mathlib

English

If f =^l g and f' =^l g', then f · f' =^l g · g'.

Русский

Если f =^l g и f' =^l g', то f · f' =^l g · g'.

LaTeX

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

Lean4

@[to_additive (attr := gcongr)]
theorem mul [Mul β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') : f * f' =ᶠ[l] g * g' :=
  h.comp₂ (· * ·) h'

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