image

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.Countable.image

← MathLib Explorer

English

If s is countable, then the image f''s of s under any function f is countable.

Русский

Если s счетно, тогда образ f''s под любой функцией f счетен.

LaTeX

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

Lean4

theorem image {s : Set α} (hs : s.Countable) (f : α → β) : (f '' s).Countable :=
  by
  rw [image_eq_range]
  have := hs.to_subtype
  apply countable_range

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

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

Разделы

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

Аффилиация

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