liftOfRightInverse_comp_apply — Mathlib

English

Equality of lifts with surjective lifting and its right inverse relation.

Русский

Равенство подъемов при сюръективном подъёме и соответствующая правая обратная связь.

LaTeX

$$$ f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) \\; \\dots $$$

Lean4

@[to_additive (attr := simp)]
theorem liftOfRightInverse_comp_apply (hf : Function.RightInverse f_inv f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker })
    (x : G₁) : (f.liftOfRightInverse f_inv hf g) (f x) = g.1 x :=
  f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x

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