nontrivial_of_image — Mathlib

English

For a surjective map, the preimage of a nonempty set is nonempty.

Русский

Для сюръективного отображения прообраз непустого множества непусто.

LaTeX

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

Lean4

/-- If the image of a set is nontrivial, the set is nontrivial. -/
theorem nontrivial_of_image (f : α → β) (s : Set α) (hs : (f '' s).Nontrivial) : s.Nontrivial :=
  let ⟨_, ⟨x, hx, rfl⟩, _, ⟨y, hy, rfl⟩, hxy⟩ := hs
  ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

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