of_finite

Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

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

English

Every finite set is semilinear.

Русский

Любое конечное множество является семилинейным.

LaTeX

$$$s.Finite \Rightarrow IsSemilinearSet s.$$$

Lean4

theorem of_finite (hs : s.Finite) : IsSemilinearSet s :=
  by
  rw [← biUnion_of_singleton s]
  apply biUnion hs
  simp

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

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

Разделы

Аффилиация

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