finite_of_encard_le

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.Finite.finite_of_encard_le

← MathLib Explorer

English

Let S be finite. If T.encard ≤ S.encard, then T is finite.

Русский

Пусть S конечен. Тогда если T.encard ≤ S.encard, то T конечен.

LaTeX

$$$\operatorname{Finite}(S) \Rightarrow (T.{encard} \le S.{encard} \Rightarrow \operatorname{Finite}(T))$$$

Lean4

theorem finite_of_encard_le {s : Set α} {t : Set β} (hs : s.Finite) (h : t.encard ≤ s.encard) : t.Finite :=
  encard_lt_top_iff.1 (h.trans_lt hs.encard_lt_top)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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