coe_trans — Mathlib

English

The coercion of a trans composition equals the composition of coerced maps.

Русский

Преобразование композиции через коэрцирование эквивалентно композиции коэрцированных отображений.

LaTeX

$$$\operatorname{coe}(e \circ e') = \operatorname{coe}(e') \circ \operatorname{coe}(e)$$$

Lean4

@[simp]
theorem coe_trans (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) : ⇑(e.trans e') = e' ∘ e :=
  rfl

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