comp_inv — Mathlib

English

If φ, ψ, χ form a CompTriple, then their underlying functions also form a CompTriple: (coe φ, coe ψ, coe χ) is a CompTriple.

Русский

Если φ, ψ, χ образуют CompTriple, то соответствующие им функции также образуют CompTriple.

LaTeX

$$$$ \text{CompTriple }(\mathrm{coe}(\varphi), \mathrm{coe}(\psi), \mathrm{coe}(\chi)). $$$$

Lean4

theorem comp_inv {φ : M →* N} {ψ : N →* M} (h : Function.RightInverse φ ψ) {χ : M →* M} [IsId χ] : CompTriple φ ψ χ
    where comp_eq := by simp only [IsId.eq_id, ← DFunLike.coe_fn_eq, coe_comp, h.id, coe_id]

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