image_eq_empty — Mathlib

English

The image of s is empty iff s is empty: f''s = ∅ ⇔ s = ∅.

Русский

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

LaTeX

$$$ f''s = \\emptyset \\ \\Leftrightarrow \\ s = \\emptyset. $$$

Lean4

@[simp, mfld_simps]
theorem image_eq_empty {α β} {f : α → β} {s : Set α} : f '' s = ∅ ↔ s = ∅ :=
  by
  simp only [eq_empty_iff_forall_notMem]
  exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩

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