mem_coe

Mathlib.Data.Part

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

English

For any a,b, a ∈ (o : Part α) ↔ a ∈ o, i.e., membership is preserved under the coe from Option to Part.

Русский

Для любых a, o: a ∈ (o : Part α) ↔ a ∈ o, т.е. принадлежность сохраняется при приведение к Part.

LaTeX

$$$ {a} \in { (o : \mathrm{Part}(\alpha)) } \iff {a} \in o $$$

Lean4

theorem mem_coe {a : α} {o : Option α} : a ∈ (o : Part α) ↔ a ∈ o :=
  mem_ofOption

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

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

Разделы

Аффилиация

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