card_le_card_of_surjOn

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_le_card_of_surjOn

← MathLib Explorer

English

If f is surjective from s onto t, then |t| ≤ |s|.

Русский

Если f отображает s на t сюръективно, то |t| ≤ |s|.

LaTeX

$$SurjOn(f, s, t) ⇒ |t| ≤ |s|$$

Lean4

theorem card_le_card_of_surjOn (f : α → β) (hf : Set.SurjOn f s t) : #t ≤ #s := by
  classical unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le

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

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

Разделы

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

Аффилиация

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