preimage — Mathlib

English

The preimage of a nontrivial set under a surjective map is nontrivial.

Русский

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

LaTeX

$$$s\text{ Nontrivial} \land f\text{ surjective } \Rightarrow (f^{-1}s).Nontrivial$.$$

Lean4

/-- The preimage of a nontrivial set under a surjective map is nontrivial. -/
theorem preimage {s : Set β} (hs : s.Nontrivial) (hf : Function.Surjective f) : (f ⁻¹' s).Nontrivial :=
  by
  rcases hs with ⟨fx, hx, fy, hy, hxy⟩
  rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
  exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

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