ofLeftInverse'_eq_ofInjective — Mathlib

English

Let f: α → β have a left inverse f_inv: β → α, with hf: LeftInverse f_inv f. Then the equivalence between α and β built from f and f_inv coincides with the injective equivalence induced by f.

Русский

Пусть f: α → β имеет левую обратную f_inv: β → α и hf: LeftInverse f_inv f. Тогда эквививелентность между α и β, построенная из f и f_inv, совпадает с эквивалентностью, индукцированной инъективностью f.

LaTeX

$$$\\operatorname{ofLeftInverse}'(f,f_{\\mathrm{inv}},hf) = \\operatorname{ofInjective}(f\\,,hf.injective)$$$

Lean4

theorem ofLeftInverse'_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : β → α) (hf : LeftInverse f_inv f) :
    ofLeftInverse' f f_inv hf = ofInjective f hf.injective :=
  by
  ext
  simp

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