invOn — Mathlib

English

For an equivalence e: α ≃ β, the pair (e, e^{-1}) forms inverses on the corresponding sets: e maps s onto t and e^{-1} maps t onto s, with e^{-1} ∘ e = id on s and e ∘ e^{-1} = id on t.

Русский

Пусть e: α ≃ β. Тогда пара (e, e^{-1}) образует обратные отображения между соответствующими множествами: e отображает s на t, а e^{-1} отображает t на s, причём e^{-1} ∘ e = id_s и e ∘ e^{-1} = id_t.

LaTeX

$$$\mathrm{InvOn}(e, e^{-1}, t, s)$$$

Lean4

theorem invOn : InvOn e e.symm t s :=
  ⟨e.rightInverse_symm.leftInvOn _, e.leftInverse_symm.leftInvOn _⟩

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