eqToIso_trans — Mathlib

English

Equality-to-iso is compatible with transitivity: composing eqToIso p with eqToIso q yields eqToIso (p trans q).

Русский

Преобразование равенства в изоморфизм совместимо с преобразованием по транзитивному объединению: композиция eqToIso p и eqToIso q равна eqToIso (p.trans q).

LaTeX

$$$ \\mathrm{eqToIso}(p) \\; \\llcorner\\!\\!\\lrcorner \\; \\mathrm{eqToIso}(q) = \\mathrm{eqToIso}(p \\; \\mathrm{trans} \\; q) $$$

Lean4

@[simp]
theorem eqToIso_trans {X Y Z : C} (p : X = Y) (q : Y = Z) : eqToIso p ≪≫ eqToIso q = eqToIso (p.trans q) := by ext; simp

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