zeroLocus_mono — Mathlib

English

If s ⊆ t are sets of sections over U, then the zero locus of t contains the zero locus of s: X.zeroLocus t ⊆ X.zeroLocus s.

Русский

Если s ⊆ t — множества секций над U, то нулевая область t содержит нулевую область s: X.zeroLocus t ⊆ X.zeroLocus s.

LaTeX

$$$s \\subseteq t \\Rightarrow X.zeroLocus(t) \\subseteq X.zeroLocus(s)$$$

Lean4

theorem zeroLocus_mono {U : X.Opens} {s t : Set Γ(X, U)} (h : s ⊆ t) : X.zeroLocus t ⊆ X.zeroLocus s :=
  by
  simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]
  exact fun x H f hf hxf ↦ H f (h hf) hxf

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