maximal_of_no_maximal — Mathlib

English

If P is not contained in any maximal ideal, then any larger proper ideal J must be the top ideal.

Русский

Если P не содержится ни в одном максимальном идеале, то любой больший proper идеал J равен ⊤.

LaTeX

$$$(\forall m, P < m \Rightarrow \neg m.IsMaximal) \Rightarrow \forall J, P < J \Rightarrow J = \top$$$

Lean4

/-- If P is not properly contained in any maximal ideal then it is not properly contained
  in any proper ideal -/
theorem maximal_of_no_maximal {P : Ideal α} (hmax : ∀ m : Ideal α, P < m → ¬IsMaximal m) (J : Ideal α) (hPJ : P < J) :
    J = ⊤ := by
  by_contra hnonmax
  rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
  exact hmax M (lt_of_lt_of_le hPJ hM2) hM1

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