image_eq_empty

Mathlib.Data.Finset.Image

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

English

The image of a set under f is empty iff the set is empty: image f s = ∅ iff s = ∅.

Русский

Образ множества s под f равен пустому множеству тогда и только тогда, когда s пусто: image f s = ∅ ↔ s = ∅.

LaTeX

$$$\mathrm{image}\ f\ s = \emptyset \iff s = \emptyset$$$

Lean4

@[simp]
theorem image_eq_empty : s.image f = ∅ ↔ s = ∅ :=
  mod_cast Set.image_eq_empty (f := f) (s := s)

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

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

Разделы

Аффилиация

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