nonempty_preimage — Mathlib

English

For a surjective map f, f^{-1}(S) is nonempty iff S is nonempty.

Русский

Для сюръективного отображения f прообраз S непуст тогда и только тогда, когда S непусто.

LaTeX

$$$(f^{-1}S).Nonempty \iff S.Nonempty$ (для сюръективного $f$).$$

Lean4

@[simp]
theorem nonempty_preimage (hf : Surjective f) {s : Set β} : (f ⁻¹' s).Nonempty ↔ s.Nonempty := by
  rw [← image_nonempty, hf.image_preimage]

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