notMem_of_compl_mem — Mathlib

English

In a Boolean algebra, if x^c ∈ I for a proper ideal I, then x ∉ I.

Русский

В булевой алгебре, если комплемент x принадлежит правильному идеалу I, то x не принадлежит I.

LaTeX

$$$ \\text{If } I \\text{ is proper and } x^c \\in I, \\text{ then } x \\notin I. $$$

Lean4

theorem notMem_of_compl_mem (hI : IsProper I) (hxc : xᶜ ∈ I) : x ∉ I :=
  by
  intro hx
  apply hI.top_notMem
  have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
  rwa [sup_compl_eq_top] at ht

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