of_image

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Infinite.of_image

English

If the image f''s of s under f is infinite, then s is infinite.

Русский

Если образ f[s] бесконечен, то и множество s бесконечно.

LaTeX

$$$ (f '' s).Infinite \Rightarrow s.Infinite $$$

Lean4

theorem of_image (f : α → β) {s : Set α} (hs : (f '' s).Infinite) : s.Infinite :=
  mt (Finite.image f) hs

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

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

Разделы

Аффилиация

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