finite_of_encard_le_coe

Mathlib.Data.Set.Card

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

English

Let k be a natural number. If encard(s) ≤ k, then s is finite.

Русский

Пусть k ∈ ℕ. Если encard(s) ≤ k, то s конечно.

LaTeX

$$$\forall k \in \mathbb{N},\ s.encard \le k \Rightarrow \operatorname{Finite}(s)$$$

Lean4

theorem finite_of_encard_le_coe {k : ℕ} (h : s.encard ≤ k) : s.Finite := by rw [← encard_lt_top_iff];
  exact h.trans_lt (WithTop.coe_lt_top _)

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

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

Разделы

Аффилиация

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