of_diff

Mathlib.Data.Set.Finite.Basic

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

English

If (S \ T) is finite and T is finite, then S is finite.

Русский

Если S \ T конечно и T конечно, тогда S конечно.

LaTeX

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

Lean4

theorem of_diff {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite :=
  (hd.union ht).subset <| subset_diff_union _ _

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

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

Разделы

Аффилиация

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