isProperSemilinearSet

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

URI: https://scilib.ai/kg/mathlib#IsProperLinearSet.isProperSemilinearSet

English

If s is a proper linear set, then s is a proper semilinear set.

Русский

Если s — правильное линейное множество, то оно является правильным семилинейным множеством.

LaTeX

$$$IsProperLinearSet(s) \Rightarrow IsProperSemilinearSet(s)$$$

Lean4

theorem isProperSemilinearSet (hs : IsProperLinearSet s) : IsProperSemilinearSet s :=
  ⟨{ s }, by simpa⟩

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

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

Разделы

Аффилиация

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