singleton

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

URI: https://scilib.ai/kg/mathlib#IsLinearSet.singleton

English

The singleton set {a} is linear.

Русский

Одночленное множество {a} линейно.

LaTeX

$$$ IsLinearSet\\{a\\} = ⟨a, \\emptyset, \\text{by simp}⟩ $$$

Lean4

@[simp]
theorem singleton (a : M) : IsLinearSet { a } :=
  ⟨a, ∅, by simp⟩

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

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

Разделы

Аффилиация

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