optionCongr_refl

Mathlib.Logic.Equiv.Option

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

English

optionCongr (refl α) equals the identity equivalence on Option α.

Русский

optionCongr (refl α) равняется тождественной эквивалентности на Option α.

LaTeX

$$$\\text{optionCongr}(\\text{refl }\\alpha) = \\text{refl }(\\text{Option }\\alpha).$$$

Lean4

@[simp]
theorem optionCongr_refl : optionCongr (Equiv.refl α) = Equiv.refl _ :=
  ext <| congr_fun Option.map_id

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

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

Разделы

Аффилиация

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