card_image_of_injOn

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#ENat.card_image_of_injOn

← MathLib Explorer

English

If f is injective on s, then the ENat.card of the image f(s) equals ENat.card s.

Русский

Если f инъективна на s, то ENat.card(образ f на s) = ENat.card(s).

LaTeX

$$$\operatorname{ENat}.card(\operatorname{Set.image} f s) = \operatorname{ENat}.card(s)$$$

Lean4

theorem card_image_of_injOn {α β : Type*} {f : α → β} {s : Set α} (h : Set.InjOn f s) : card (f '' s) = card s :=
  card_congr (Equiv.Set.imageOfInjOn f s h).symm

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

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

Разделы

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

Аффилиация

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