coe_toEquiv_trans — Mathlib

English

The underlying Equiv of the forward direction of the transitive equivalence matches the transitive Equiv of the forward directions.

Русский

Базовое эквивалентное отображение перехода через транзитивную эквивалентность согласуется с транспонированной эквивалентностью прямых направлений.

LaTeX

$$$ (e_{12} : A \\simeq B) .\\mathrm{trans} e_{23} = (e_{12}.trans e_{23} : A \\simeq C)$$$

Lean4

@[simp]
theorem coe_toEquiv_trans : (e₁₂ : A ≃ B).trans e₂₃ = (e₁₂.trans e₂₃ : A ≃ C) :=
  rfl

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