diff

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Infinite.diff

English

If s is infinite and t is finite, then s \ t is infinite.

Русский

Если s бесконечно, а t конечно, то s \ t бесконечно.

LaTeX

$$$ s\ \ t \text{ Infinite} \quad (hs:\, s\ Infinite,\ ht:\, t\ Finite) $$$

Lean4

theorem diff {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : (s \ t).Infinite := fun h => hs <| h.of_diff ht

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

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

Разделы

Аффилиация

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