isMaximal_iff — Mathlib

English

Let I be an ideal in α. Then I is maximal if and only if 1 ∉ I and, for every J ≥ I and every x ∉ I, if x ∈ J then 1 ∈ J.

Русский

Пусть I — идеал в α. Тогда I максимален тогда и только тогда, когда 1 ∉ I и для любого J ≥ I и любого x ∉ I, если x ∈ J, то 1 ∈ J.

LaTeX

$$$I\ IsMaximal \iff \bigl(1 \notin I\bigr) \land \forall J:\ Ideal\ α\,\forall x:\ α,\ I \le J \rightarrow x \notin I \rightarrow x \in J \rightarrow 1 \in J$$$

Lean4

theorem isMaximal_iff {I : Ideal α} :
    I.IsMaximal ↔ (1 : α) ∉ I ∧ ∀ (J : Ideal α) (x), I ≤ J → x ∉ I → x ∈ J → (1 : α) ∈ J := by
  simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]

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