isMaximal — Mathlib

English

In a Boolean algebra, if I is prime then I is maximal.

Русский

В булевой алгебре простота I влечёт максимальность I.

LaTeX

$$$IsPrime I \\Rightarrow IsMaximal I$$$

Lean4

instance (priority := 100) isMaximal [IsPrime I] : IsMaximal I :=
  by
  simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
  intro J hIJ x
  rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
  suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
  exact sup_mem (J.lower inf_le_right hyJ) (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)

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