ideal_ext_iff — Mathlib

English

Two ideals I and J in Γ(X,U) are equal if and only if their images under all germ maps agree.

Русский

Два идеала I и J в Γ(X,U) равны тогда и только тогда, когда их образы через все гёрм-отображения совпадают.

LaTeX

$$$I = J \iff \forall x\in X,\forall h\in U, I.map( X.presheaf.germ U x h).hom = J.map( X.presheaf.germ U x h).hom$$$

Lean4

theorem ideal_ext_iff {I J : Ideal Γ(X, U)} :
    I = J ↔ ∀ (x : X) (h : x ∈ U), I.map (X.presheaf.germ U x h).hom = J.map (X.presheaf.germ U x h).hom := by
  simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]

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