finite_of_ncard_ne_zero

Mathlib.Data.Set.Card

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

English

If a subset s has ncard not equal to zero, then s is finite.

Русский

Если кардинал подмножества s не равен нулю, то s конечен.

LaTeX

$$$ s.ncard \neq 0 \Rightarrow s \text{ is finite} $$$

Lean4

theorem finite_of_ncard_ne_zero (hs : s.ncard ≠ 0) : s.Finite :=
  s.finite_or_infinite.elim id fun h ↦ (hs h.ncard).elim

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

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

Разделы

Аффилиация

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