of_toOption

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.of_toOption

English

For any o, the composite ofOption ∘ toOption is the identity on Part: ofOption (toOption o) = o.

Русский

Для любого o, композиция ofOption ∘ toOption является тождественной на Part: ofOption (toOption o) = o.

LaTeX

$$$ \mathrm{ofOption}(\mathrm{toOption}(o)) = o $$$

Lean4

@[simp]
theorem of_toOption (o : Part α) [Decidable o.Dom] : ofOption (toOption o) = o :=
  ext fun _ => mem_ofOption.trans mem_toOption

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

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

Разделы

Аффилиация

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