fun_inv — Mathlib

English

If f =^l g, then (fun x => inv (f x)) =^l (fun x => inv (g x)).

Русский

Если f =^l g, то функция, применяющая инверсию к значению, сохраняет эквивалентность.

LaTeX

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

Lean4

@[to_additive]
theorem fun_inv [Inv β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : (fun x => (f x)⁻¹) =ᶠ[l] fun x => (g x)⁻¹ :=
  h.inv

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