encard_image

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Function.Injective.encard_image

English

If f is injective, then encard(image f s) = encard(s).

Русский

Если f инъективно, то энкарда образа f на s равна энкарде s.

LaTeX

$$$ (f'' s).encard = s.encard $$$

Lean4

theorem _root_.Function.Injective.encard_image (hf : f.Injective) (s : Set α) : (f '' s).encard = s.encard :=
  hf.injOn.encard_image

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

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

Разделы

Аффилиация

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