of_mem_or_mem — Mathlib

English

If [IsProper I] and for all x,y, x ⊓ y ∈ I implies x ∈ I or y ∈ I, then I is prime.

Русский

Если I является правильным и выполняется условие о металиновом разложении, то I — простый.

LaTeX

$$$[IsProper\\ I]\\; (\\forall x\\, y:\\; x \\land y \\in I \\Rightarrow x \\in I \\lor y \\in I) \\Rightarrow IsPrime I$$$

Lean4

theorem of_mem_or_mem [IsProper I] (hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I) : IsPrime I :=
  by
  rw [isPrime_iff]
  use ‹_›
  refine .of_def ?_ ?_ ?_
  · exact Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›)
  · intro x hx y hy
    exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩
  · exact @mem_compl_of_ge _ _ _

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