isProper_of_notMem — Mathlib

English

If an element p does not belong to an ideal I of P, then I is a proper ideal (i.e., I ≠ ⊤).

Русский

Если элемент p не принадлежит идеалу I в P, то I является правильным идеалом (то есть I ≠ ⊤).

LaTeX

$$$p \notin I \Rightarrow I \neq \top$$$

Lean4

theorem isProper_of_notMem {I : Ideal P} {p : P} (notMem : p ∉ I) : IsProper I :=
  ⟨fun hp ↦ by
    have := mem_univ p
    rw [← hp] at this
    exact notMem this⟩

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