le_def — Mathlib

English

For two ideal sheaf data I and J on a scheme X, I ≤ J if and only if for every affine open U of X, the inclusion I.ideal(U) ≤ J.ideal(U) holds.

Русский

Для двух данных идеала на схеме X верно: I ≤ J тогда и только тогда, когда для каждого аффинного открытого U выполняется I.ideal(U) ⊆ J.ideal(U).

LaTeX

$$$ I \le J \iff \forall U, I.ideal(U) \le J.ideal(U) $$$

Lean4

theorem le_def {I J : IdealSheafData X} : I ≤ J ↔ ∀ U, I.ideal U ≤ J.ideal U :=
  .rfl

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