ne_top_iff_exists_maximal — Mathlib

English

An ideal I is not the top if and only if there exists a maximal ideal M with I ≤ M.

Русский

Идеал I не равен ⊤ тогда и только тогда, когда существует максимальный идеал M с I ≤ M.

LaTeX

$$$I \neq \top \iff \exists M:\ Ideal\ α, M.IsMaximal \land I \le M$$$

Lean4

theorem ne_top_iff_exists_maximal {I : Ideal α} : I ≠ ⊤ ↔ ∃ M : Ideal α, M.IsMaximal ∧ I ≤ M :=
  by
  refine ⟨exists_le_maximal I, ?_⟩
  contrapose!
  rintro rfl _ hMmax
  rw [top_le_iff]
  exact IsMaximal.ne_top hMmax

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