liftOfRightInverseAux_comp_apply — Mathlib

English

For any x in G1, applying the lifted map to f(x) yields g(x).

Русский

Для любого x в G1 применение поднимаемой отображения к f(x) даёт g(x).

LaTeX

$$$ (f.liftOfRightInverse f^{-1} hf g) (f x) = g x \\quad (x \\in G1) $$$

Lean4

@[to_additive (attr := simp)]
theorem liftOfRightInverseAux_comp_apply (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker)
    (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x :=
  by
  dsimp [liftOfRightInverseAux]
  rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
  apply hg
  rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]
  simp only [hf _]

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