eq_none_iff'

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.eq_none_iff'

English

A Part o equals none if and only if its domain is false; equivalently, ¬ o.Dom.

Русский

Часть o равна none тогда и только тогда, когда её область определения ложна; равносильно ¬ o.Dom.

LaTeX

$$$$o = \mathrm{none} \iff \neg o.Dom.$$$$

Lean4

theorem eq_none_iff' {o : Part α} : o = none ↔ ¬o.Dom :=
  ⟨fun e => e.symm ▸ id, fun h => eq_none_iff.2 fun _ h' => h h'.fst⟩

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

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

Разделы

Аффилиация

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