ncard_image_of_injOn

Mathlib.Data.Set.Card

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

English

If f is injective on s, then the image f''s has the same cardinality as s.

Русский

Если f инъективна на s, то образ f''s имеет ту же кардинал, что и s.

LaTeX

$$$ \text{(H : Set.InjOn f s)} \Rightarrow (f '' s).ncard = s.ncard $$$

Lean4

theorem ncard_image_of_injOn (H : Set.InjOn f s) : (f '' s).ncard = s.ncard :=
  congr_arg ENat.toNat <| H.encard_image

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

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

Разделы

Аффилиация

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