closure_of_finite

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

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

English

If s is finite, then closure s is linear.

Русский

Если s конечное, то closure s линейно.

LaTeX

$$$ (hs : s.Finite) \\rightarrow IsLinearSet (closure s : Set M) $$$

Lean4

theorem closure_of_finite (hs : s.Finite) : IsLinearSet (closure s : Set M) :=
  ⟨0, s, hs, by simp⟩

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

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

Разделы

Аффилиация

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