fun_div — Mathlib

English

If f =^l g and f' =^l g', then (fun x => f x / f' x) =^l (fun x => g x / g' x).

Русский

Если f =^l g и f' =^l g', то (f x)/(f' x) =^l (g x)/(g' x).

LaTeX

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

Lean4

@[to_additive]
theorem fun_div [Div β] {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.div h'

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