toOption_eq_some_iff

Mathlib.Data.Part

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

← MathLib Explorer

English

For any a ∈ Part α, a.toOption = None iff not a.Dom.

Русский

Для любого a ∈ Part α, a.toOption = None тогда и только тогда, когда не выполняется a.Dom.

LaTeX

$$$ a.\\toOption = \\mathrm{Option.none} \\Leftrightarrow \\neg a.\\Dom $$$

Lean4

@[simp]
theorem toOption_eq_some_iff {o : Part α} [Decidable o.Dom] {a : α} : toOption o = Option.some a ↔ a ∈ o := by
  rw [← Option.mem_def, mem_toOption]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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