vanishingIdeal_empty

Mathlib.RingTheory.Nullstellensatz

URI: https://scilib.ai/kg/mathlib#MvPolynomial.vanishingIdeal_empty

English

vanishingIdeal of the empty set is the top ideal.

Русский

vanishingIdeal пустого множества — верхний идеал.

LaTeX

$$$\\mathrm{vanishingIdeal}(k, \\varnothing) = \\top$$$

Lean4

theorem vanishingIdeal_empty : vanishingIdeal k (∅ : Set (σ → K)) = ⊤ :=
  le_antisymm le_top fun _ _ x hx => absurd hx (Set.notMem_empty x)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru