image_nonempty

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.image_nonempty

English

For any embedding f and Finset s, (image f s).Nonempty ↔ s.Nonempty.

Русский

Для любого вложения f и множества s: (image f s).Nonempty эквивалентно s.Nonempty.

LaTeX

$$$\\operatorname{Nonempty}(\\operatorname{image}(f,s)) \\iff \\operatorname{Nonempty}(s)$$$

Lean4

@[simp]
theorem image_nonempty : (s.image f).Nonempty ↔ s.Nonempty :=
  mod_cast Set.image_nonempty (f := f) (s := (s : Set α))

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

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

Разделы

Аффилиация

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