notMem_or_compl_notMem

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.IsProper.notMem_or_compl_notMem

English

For a proper ideal I in a Boolean algebra, either x ∉ I or x^c ∉ I.

Русский

Для правильного идеала I в булевой алгебре либо x ∉ I, либо x^c ∉ I.

LaTeX

$$$ \text{If } I \\text{ is proper}, \quad x \notin I \lor x^c \notin I. $$$

Lean4

theorem notMem_or_compl_notMem (hI : IsProper I) : x ∉ I ∨ xᶜ ∉ I :=
  by
  have h : xᶜ ∈ I → x ∉ I := hI.notMem_of_compl_mem
  tauto

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

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

Разделы

Аффилиация

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