nontrivial_of_preimage — Mathlib

English

If the preimage of a set under an injective map is nontrivial, then the set is nontrivial.

Русский

Если прообраз множества по инъективному отображению не тривиален, то и само множество не тривиально.

LaTeX

$$$(f^{-1}s).Nontrivial \Rightarrow s.Nontrivial$ при $f$ инъективном.$$

Lean4

/-- If the preimage of a set under an injective map is nontrivial, the set is nontrivial. -/
theorem nontrivial_of_preimage (hf : Function.Injective f) (s : Set β) (hs : (f ⁻¹' s).Nontrivial) : s.Nontrivial :=
  (hs.image hf).mono <| image_preimage_subset _ _

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