sup

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.sup

English

Finite union is finite (supremum of sets).

Русский

Конечное объединение любых двух конечных множеств является конечным.

LaTeX

$$$\forall {\alpha : Type u} {s t : Set\alpha}, Finite s → Finite t → Finite (s \sqcup t)$$$

Lean4

theorem sup {s t : Set α} : s.Finite → t.Finite → (s ⊔ t).Finite :=
  Finite.union

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

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

Разделы

Аффилиация

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