card_image_le

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_image_le

← MathLib Explorer

English

If s.Finite, Nat.card (f '' s) ≤ Nat.card s.

Русский

Если s конечно, Nat.card (f '' s) ≤ Nat.card s.

LaTeX

$$$ (s . \mathrm{Finite}) \rightarrow \mathrm{Nat.card}(\mathrm{Set.image}\,f\,s) \le \mathrm{Nat.card}\,s $$$

Lean4

theorem card_image_le {f : α → β} (hs : s.Finite) : Nat.card (f '' s) ≤ Nat.card s :=
  have := hs.to_subtype
  card_le_card_of_surjective (imageFactorization f s) imageFactorization_surjective

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

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

Разделы

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

Аффилиация

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