countable_of_injective_of_countable_image

Mathlib.Data.Set.Countable

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

← MathLib Explorer

English

If InjOn f s and (f '' s) is countable, then s is countable.

Русский

Если InjOn f s и образ f(s) счетен, то s счетно.

LaTeX

$$$\\operatorname{InjOn}(f,s) \\Rightarrow (f''s) \\text{ Countable } \\Rightarrow s \\text{ Countable}$$$

Lean4

theorem countable_of_injective_of_countable_image {s : Set α} {f : α → β} (hf : InjOn f s) (hs : (f '' s).Countable) :
    s.Countable :=
  (mapsTo_image _ _).countable_of_injOn hf hs

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

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

Разделы

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

Аффилиация

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