liftOfRightInverse_eq — Mathlib

English

If hf1 and hf2 are right inverses of the same f, then the corresponding lifts of right inverse coincide: liftOfRightInverse hf1 hd = liftOfRightInverse hf2 hd.

Русский

Если hf1 и hf2 — правые образы обратные одному и тому же f, тогда соответствующие подъемы через правый обратный совпадают: liftOfRightInverse hf1 hd = liftOfRightInverse hf2 hd.

LaTeX

$$$\operatorname{liftOfRightInverse}(hf_1, hd) = \operatorname{liftOfRightInverse}(hf_2, hd)$$$

Lean4

theorem liftOfRightInverse_eq {f : F} {f_inv₁ f_inv₂ : M → A} (hf₁ : Function.RightInverse f_inv₁ f)
    (hf₂ : Function.RightInverse f_inv₂ f) : liftOfRightInverse hf₁ = liftOfRightInverse hf₂ :=
  by
  ext _ _ x
  obtain ⟨x, rfl⟩ := hf₁.surjective x
  simp

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