inv — Mathlib

English

If u ~_l v, then u^{-1} ~_l v^{-1}.

Русский

Если u эквивалентно v по l, то их обратные по л также эквивалентны.

LaTeX

$$$ u \\sim_{l} v \\Rightarrow u^{-1} \\sim_{l} v^{-1} $$$

Lean4

protected theorem inv (huv : u ~[l] v) : u⁻¹ ~[l] v⁻¹ :=
  by
  rw [isEquivalent_iff_exists_eq_mul] at *
  rcases huv with ⟨φ, hφ, h⟩
  rw [← inv_one]
  refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by simp), ?_⟩
  convert h.fun_inv
  simp [mul_comm]

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