English
In a disjointness context with disjointness between I and S, there exists a prime p with I ≤ p and p disjoint from S, as above.
Русский
В контексте несовпадения существует prime p с I ≤ p и p дисjoint от S.
LaTeX
$$$\\exists p:\\; p.IsPrime \\land I \\le p \\land Disjoint (p) (S).$$$
Lean4
theorem exists_le_prime_disjoint (S : Submonoid α) (disjoint : Disjoint (I : Set α) S) :
∃ p : Ideal α, p.IsPrime ∧ I ≤ p ∧ Disjoint (p : Set α) S :=
by
have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S} (fun c hc hc' x hx ↦ ?_) I disjoint
· exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩
cases isEmpty_or_nonempty c
· exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩
refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩
have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)
exact Set.disjoint_left.mp (hc p.2) hp
