nonempty_apply_iff — Mathlib

English

If f is injective and sends the empty set to the empty set, then for any s, (f s) is nonempty iff s is nonempty.

Русский

Если f инъективна и отображает пустое множество в пустое, тогда для любого s, (f s) непусто ⇔ s непусто.

LaTeX

$$$ (f \\ s).Nonempty \\iff s.Nonempty $$$

Lean4

theorem nonempty_apply_iff {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅) {s : Set α} :
    (f s).Nonempty ↔ s.Nonempty := by rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

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