forall_of_forall_prime — Mathlib

English

If every prime ideal satisfies P and there exists a maximal counterexample to P, then all ideals satisfy P.

Русский

Если все простые идеалы удовлетворяют P и существует максимальный контрпример P, то все идеалы удовлетворяют P.

LaTeX

$$IsOka statement$$

Lean4

/-- If a ring `R` verify:
1. All prime ideals of `R` satisfy an Oka predicate `P`.
2. One ideal not satisfying `P` implies that there is an ideal maximal for not satisfying `P`.

Then all the ideals of `R` satisfy `P`. -/
theorem forall_of_forall_prime (hmax : ∀ I, ¬P I → ∃ I, Maximal (¬P ·) I) (hprime : ∀ I, I.IsPrime → P I)
    (I : Ideal R) : P I := by
  by_contra! hI
  obtain ⟨I, hI⟩ := hmax I hI
  exact hI.prop <| hprime I (hP.isPrime_of_maximal_not hI)

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