refl_trans — Mathlib

English

The left identity element acts as a left identity for composition: (Equiv.refl α).trans e = e.

Русский

Левый тождественный элемент действует как левый тождественный элемент по отношению к композиции: (Equiv.refl α).trans e = e.

LaTeX

$$$(\\mathrm{Equiv.refl }\\alpha).trans\,e = e$$$

Lean4

@[simp]
theorem refl_trans (e : α ≃ β) : (Equiv.refl α).trans e = e := by cases e; rfl

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