div — 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',g,g' : \\\\alpha \\\\to \\\\beta \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\ (f =^l g) \\\\Rightarrow \\\\ (f' =^l g') \\\\Rightarrow \\\\bigl((f / f') =^l (g / g')\\\\bigr)$$$

Lean4

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

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