encard_range

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

If f is injective, then ENat.card of α is ≤ encard of range f.

Русский

Пусть f инъективно, тогда ENat.card(α) ≤ encard(range f).

LaTeX

$$$ ENat.card\\alpha \\le (range\, f).encard $$$

Lean4

theorem _root_.Function.Injective.encard_range (hf : f.Injective) : ENat.card α ≤ (range f).encard := by
  rw [← image_univ, hf.encard_image, encard_univ]

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

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

Разделы

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

Аффилиация

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