vanishingIdeal_sup — Mathlib

English

Vanishing ideal respects lattice operations: vanishingIdeal(Z ⊔ Z') = vanishingIdeal(Z) ⊓ vanishingIdeal(Z').

Русский

Идеал исчезновения сохраняет операции соединения: vanishingIdeal(Z ⊔ Z') = vanishingIdeal(Z) ⊓ vanishingIdeal(Z').

LaTeX

$$\\operatorname{vanishingIdeal}(Z \\sqcup Z') = \\operatorname{vanishingIdeal}(Z) \\cap \\operatorname{vanishingIdeal}(Z')$$

Lean4

@[simp]
theorem vanishingIdeal_sup (Z Z' : TopologicalSpace.Closeds X) :
    vanishingIdeal (Z ⊔ Z') = vanishingIdeal Z ⊓ vanishingIdeal Z' :=
  gc.u_inf

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