finite_of_encard_eq_coe

Mathlib.Data.Set.Card

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

English

If encard(s) equals a natural number k, then s is finite.

Русский

Если encard(s) равно натуральному числу k, то S конечно.

LaTeX

$$$s.encard = k \Rightarrow \operatorname{Finite}(s)$$$

Lean4

theorem finite_of_encard_eq_coe {k : ℕ} (h : s.encard = k) : s.Finite :=
  finite_of_encard_le_coe h.le

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

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

Разделы

Аффилиация

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