isPrime_of_mem_or_compl_mem — Mathlib

English

If every element x satisfies x ∈ I or xᶜ ∈ I and I is proper, then I is prime.

Русский

Если для всех x выполняется x ∈ I или xᶜ ∈ I и I является proper, то I прост.

LaTeX

$$$\\text{IsProper}(I) \\; \\&\\; (\\forall x, x \\in I \\lor x^c \\in I) \\Rightarrow IsPrime I$$$

Lean4

theorem isPrime_of_mem_or_compl_mem [IsProper I] (h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I) : IsPrime I :=
  by
  simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]
  intro x y hxy hxI
  have hxcI : xᶜ ∈ I := h.resolve_left hxI
  have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
  rwa [inf_comm, sup_inf_inf_compl] at ass

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