finite_of_ncard_pos

Mathlib.Data.Set.Card

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

English

If 0 < s.ncard then s is finite.

Русский

Если 0 < ncard(s), то s конечен.

LaTeX

$$$ 0 < s.ncard \Rightarrow s \text{ finite} $$$

Lean4

theorem finite_of_ncard_pos (hs : 0 < s.ncard) : s.Finite :=
  finite_of_ncard_ne_zero hs.ne.symm

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

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

Разделы

Аффилиация

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