card_range_of_injective

Mathlib.SetTheory.Cardinal.Finite

URI: https://scilib.ai/kg/mathlib#Nat.card_range_of_injective

← MathLib Explorer

English

If f : α → β is injective, then Nat.card(range f) = Nat.card α.

Русский

Если f : α → β инъективно, то Nat.card(range f) = Nat.card α.

LaTeX

$$$$ |\operatorname{range}(f)| = |\alpha| $$$$

Lean4

theorem card_range_of_injective {f : α → β} (hf : Injective f) : Nat.card (range f) = Nat.card α :=
  by
  rw [← Nat.card_preimage_of_injective hf le_rfl]
  simp [Nat.card_univ]

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

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

Разделы

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

Аффилиация

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