image_nonempty

Mathlib.Data.Set.Image

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

English

The image of S is nonempty if and only if S is nonempty.

Русский

Образ S непуст тогда и только тогда, когда S непуст.

LaTeX

$$$$ (f[S]).\Nonempty \iff S.\Nonempty. $$$$

Lean4

@[simp]
theorem image_nonempty {f : α → β} {s : Set α} : (f '' s).Nonempty ↔ s.Nonempty :=
  ⟨Nonempty.of_image, fun h => h.image f⟩

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

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

Разделы

Аффилиация

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