fun_mul — Mathlib

English

If f₁ =^l f₂, then f₃ · f₁ =^l f₃ · f₂.

Русский

Если f₁ =^l f₂, то f₃ · f₁ =^l f₃ · f₂.

LaTeX

$$$\\\\forall f₁,f₂,f₃ : \\\\alpha \\\\to \\\\beta, \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\ (f₁ =^l f₂) \\\\Rightarrow \\\\bigl((f₃ \\\\cdot f₁) =^l (f₃ \\\\cdot f₂)\\\\bigr)$$$

Lean4

@[to_additive]
theorem fun_mul [Mul β] {f f' g g' : α → β} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
    (fun x => f x * f' x) =ᶠ[l] fun x => g x * g' x :=
  h.mul h'

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