finsetCongr_refl — Mathlib

English

The congruence induced by the identity bijection is the identity congruence on Finset.

Русский

Образующая конгруэнтность от тождестенного биекции в Finset дает тождественную конгруэнтность.

LaTeX

$$$(\\mathrm{Equiv.refl}\\; \\alpha).\\mathrm{finsetCongr} = \\mathrm{Equiv.refl}\\(\\mathrm{Finset}(\\alpha))$$$

Lean4

@[simp]
theorem finsetCongr_refl : (Equiv.refl α).finsetCongr = Equiv.refl _ :=
  by
  ext
  simp

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