ncard_image_of_injective

Mathlib.Data.Set.Card

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

English

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

Русский

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

LaTeX

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

Lean4

theorem ncard_image_of_injective (s : Set α) (H : f.Injective) : (f '' s).ncard = s.ncard :=
  ncard_image_of_injOn fun _ _ _ _ h ↦ H h

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

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

Разделы

Аффилиация

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