extendDomain_one — Mathlib

English

For any f: α ≃ Subtype p, extending the domain of the identity permutation gives the identity on α: extendDomain 1 f = 1.

Русский

Для любого f: α ≃ {x | p x} расширение области определения единичной перестановки даёт тождественную перестановку на α: extendDomain 1 f = 1.

LaTeX

$$$$ \mathrm{extendDomain\_one} : \mathrm{extendDomain}(1,f)=1. $$$$

Lean4

@[simp]
theorem extendDomain_one : extendDomain 1 f = 1 :=
  extendDomain_refl f

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