withBotCongr_refl

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#Equiv.withBotCongr_refl

English

The congruence induced by the identity equivalence is the identity on WithBot.

Русский

Сведение, порождаемое тождественной эквив, даёт тождественное отображение на WithBot.

LaTeX

$$$\text{withBotCongr} (\mathrm{Equiv.refl}\ α) = \mathrm{Equiv.refl}\ (WithBot\ α)$$$

Lean4

@[simp]
theorem withBotCongr_refl : withBotCongr (Equiv.refl α) = Equiv.refl _ :=
  Equiv.ext <| congr_fun WithBot.map_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru