inv — Mathlib

English

If f =^l g, then f⁻¹ =^l g⁻¹ for functions into β with Inv structure.

Русский

Если f =^l g, то f⁻¹ =^l g⁻¹ для функций с наличием операции инверсии.

LaTeX

$$$\\\\forall f,g : \\\\alpha \\\\to \\\\beta \\\\forall l \\\\ (l : Filter \\\\alpha), \\\\ (f =^l g) \\\\Rightarrow \\\\ (f^{-1} =^l g^{-1})$$$

Lean4

@[to_additive (attr := gcongr)]
theorem inv [Inv β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) : f⁻¹ =ᶠ[l] g⁻¹ :=
  h.fun_comp Inv.inv

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