English
If s is a nonempty chain of prime ideals, then their infimum (intersection) is prime.
Русский
Если s — непустая цепь простых идеалов, то их нижняя граница (пересечение) — простый идеал.
LaTeX
$$$s \neq \emptyset \land IsChain(\le)\ s \land (\forall p\in s, p.IsPrime) \Rightarrow (\inf s).IsPrime$$
Lean4
theorem sInf_isPrime_of_isChain {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (· ≤ ·) s)
(H : ∀ p ∈ s, p.IsPrime) : (sInf s).IsPrime :=
⟨fun e =>
let ⟨x, hx⟩ := hs
(H x hx).ne_top (eq_top_iff.mpr (e.symm.trans_le (sInf_le hx))),
fun e =>
or_iff_not_imp_left.mpr fun hx => by
rw [Ideal.mem_sInf] at hx e ⊢
push_neg at hx
obtain ⟨I, hI, hI'⟩ := hx
intro J hJ
rcases hs'.total hI hJ with h | h
· exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')
· exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x⟩
