ncard_map

Mathlib.Data.Set.Card

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

English

For an embedding f, the image of s has the same cardinality as s.

Русский

Для вложения (embeding) f образ s имеет ту же кардинал, что и s.

LaTeX

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

Lean4

@[simp]
theorem ncard_map (f : α ↪ β) : (f '' s).ncard = s.ncard :=
  ncard_image_of_injective _ f.inj'

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

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

Разделы

Аффилиация

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