part_eq_empty

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.part_eq_empty

English

P.part a equals the empty set if and only if a is not in s.

Русский

P.part a равно пустому множества тогда и только тогда, когда a не принадлежит s.

LaTeX

$$$ P.part a = \emptyset \iff a \notin s $$$

Lean4

@[simp]
theorem part_eq_empty : P.part a = ∅ ↔ a ∉ s :=
  ⟨fun h has ↦ P.ne_empty (P.part_mem.2 has) h, fun h ↦ by simp [part, h]⟩

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

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

Разделы

Аффилиация

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