preimage' — Mathlib

English

If the intersection of s with the range of f is infinite, then f^{-1}(s) is infinite.

Русский

Если пересечение s с диапазоном f бесконечно, то прообраз бесконечен.

LaTeX

$$$\bigl(s \cap \mathrm{range}(f)\bigr) \text{ infinite} \Rightarrow f^{-1}(s) \text{ infinite}$$$

Lean4

theorem preimage' (hs : (s ∩ range f).Infinite) : (f ⁻¹' s).Infinite :=
  (hs.preimage inter_subset_right).mono <| preimage_mono inter_subset_left

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