infinite_coe_iff

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Set.infinite_coe_iff

English

The infiniteness of a set s equals the infiniteness of its underlying type s.Elem (the subtype).

Русский

Бесконечность множества s равна бесконечности его подтипа s.Elem.

LaTeX

$$$ \\text{Infinite}(s) \\iff \\text{Infinite}(s^{\\text{Elem}}) $$$

Lean4

theorem infinite_coe_iff {s : Set α} : Infinite s ↔ s.Infinite :=
  not_finite_iff_infinite.symm.trans finite_coe_iff.not

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

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

Разделы

Аффилиация

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