mem_or_compl_mem

Mathlib.Order.PrimeIdeal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.IsPrime.mem_or_compl_mem

English

In a Boolean algebra, if I is prime then every element x is in I or its complement is in I.

Русский

В булевой алгебре, если I простый, то для каждого x либо x ∈ I, либо xᶜ ∈ I.

LaTeX

$$$\\forall x:\\; x \\in I \\lor x^c \\in I$$$

Lean4

theorem mem_or_compl_mem (hI : IsPrime I) : x ∈ I ∨ xᶜ ∈ I :=
  by
  apply hI.mem_or_mem
  rw [inf_compl_eq_bot]
  exact I.bot_mem

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

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

Разделы

Аффилиация

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