zeroLocus_union — Mathlib

English

The vanishing locus of a union of two sets equals the intersection of the vanishing loci of each set.

Русский

Нуль-множество объединения двух множеств равно пересечению нуль-множества каждого множества.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(s \cup s') = \operatorname{zeroLocus}_{\mathcal{A}}(s) \cap \operatorname{zeroLocus}_{\mathcal{A}}(s') $$$

Lean4

theorem zeroLocus_union (s s' : Set A) : zeroLocus 𝒜 (s ∪ s') = zeroLocus _ s ∩ zeroLocus _ s' :=
  (gc_set 𝒜).l_sup

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