singleton

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

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

English

For any a ∈ M, {a} is semilinear.

Русский

Для любого a ∈ M множество {a} семилинейно.

LaTeX

$$$IsSemilinearSet({a}).$$$

Lean4

@[simp]
theorem singleton (a : M) : IsSemilinearSet { a } :=
  (IsLinearSet.singleton a).isSemilinearSet

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

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

Разделы

Аффилиация

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