card_preimage_of_injective

Mathlib.SetTheory.Cardinal.Finite

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

← MathLib Explorer

English

If f : α → β is injective and S ⊆ range f, then Nat.card(f⁻¹(S)) = Nat.card(S).

Русский

Пусть f : α → β инъективно, и S ⊆ range f. Тогда card(f⁻¹(S)) = card(S).

LaTeX

$$$$ |f^{-1}(S)| = |S| $$$$

Lean4

theorem card_preimage_of_injective {f : α → β} {s : Set β} (hf : Injective f) (hsf : s ⊆ range f) :
    Nat.card (f ⁻¹' s) = Nat.card s :=
  card_preimage_of_injOn hf.injOn hsf

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

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

Разделы

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

Аффилиация

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