eq_of_le — Mathlib

English

If I is maximal, J ≠ ⊤, and I ≤ J, then I = J: a maximal ideal cannot be strictly contained in a proper larger ideal.

Русский

Если I максимален, и J ≠ ⊤, и I ⊆ J, то I = J: максимальный идеал не может быть строго вложен в другой proper идеал.

LaTeX

$$$I \text{ maximal} \land J \neq \top \land I \le J \Rightarrow I = J$$$

Lean4

theorem eq_of_le {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J :=
  eq_iff_le_not_lt.2 ⟨IJ, fun h => hJ (hI.1.2 _ h)⟩

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