trans_refl — Mathlib

English

The forward direction composed with identity on the right yields the original pseudoequivalence: f.trans (PEquiv.refl β) = f.

Русский

Преходящая композиция с тождеством слева/справа даёт исходную псевдоэквивалентность: f.trans (PEquiv.refl β) = f.

LaTeX

$$$$ f.trans (\\mathrm{PEquiv.refl}\\ \\beta) = f. $$$$

Lean4

@[simp]
theorem trans_refl (f : α ≃. β) : f.trans (PEquiv.refl β) = f := by ext; dsimp [PEquiv.trans]; simp

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