isPrime_iff_mem_or_mem — Mathlib

English

In a Boolean algebra, for a proper ideal I, IsPrime I iff for every x, x ∈ I or xᶜ ∈ I.

Русский

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

LaTeX

$$$[IsProper I] : IsPrime I \\iff ∀ x:\\; x \\in I \\lor x^c \\in I$$$

Lean4

theorem isPrime_iff_mem_or_mem [IsProper I] : IsPrime I ↔ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I :=
  ⟨IsPrime.mem_or_mem, IsPrime.of_mem_or_mem⟩

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