map_nonempty — Mathlib

English

Let f be an embedding and s a finite set. Then (image f s) is nonempty if and only if s is nonempty.

Русский

Пусть f — инъекция и s — конечное множество. Тогда образ f(s) непуст тогда и только тогда, когда s непусто.

LaTeX

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

Lean4

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

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