equivShrink_symm_one — Mathlib

English

Let α be a type with a Shrink equivalence. Then the inverse of this equivalence sends the identity element to itself: (equivShrink α)^{-1} 1 = 1.

Русский

Пусть α — тип с эквивалентным отображением Shrink. Тогда обратное отображение этого эквивалента отправляет единицу в единицу: (equivShrink α)^{-1} 1 = 1.

LaTeX

$$$(\operatorname{equivShrink} \alpha)^{-1}(1) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem equivShrink_symm_one [One α] : (equivShrink α).symm 1 = 1 :=
  (equivShrink α).symm_apply_apply 1

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