trans_one — Mathlib

English

For any α and any e ∈ Perm α, e ∘ 1 = e, i.e. composing with the identity permutation leaves e unchanged.

Русский

Для любого α и любого e ∈ Perm α выполняется e ∘ 1 = e, то есть композиция с тождественной перестановкой не меняет e.

LaTeX

$$$\\\\forall {\\alpha} {e : \\\\mathrm{Perm} \\\\alpha}, \\\\; e \\\\circ 1 = e$$$

Lean4

@[simp]
theorem trans_one {α : Sort*} {β : Type*} (e : α ≃ β) : e.trans (1 : Perm β) = e :=
  Equiv.trans_refl e

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