eq_none_iff

Mathlib.Data.Part

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

English

A Part o is equal to none if and only if every element is not in o.

Русский

Часть o равна none тогда и только тогда, когда для каждого элемента он не принадлежит o.

LaTeX

$$$$o = \mathrm{none} \iff \forall a, a \notin o.$$$$

Lean4

theorem eq_none_iff {o : Part α} : o = none ↔ ∀ a, a ∉ o :=
  ⟨fun e => e.symm ▸ notMem_none, fun h => ext (by simpa)⟩

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

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

Разделы

Аффилиация

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