preimage — Mathlib

English

If s is infinite and s is contained in range f, then f^{-1}(s) is infinite.

Русский

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

LaTeX

$$$s \text{ infinite} \land s \subseteq \mathrm{range}(f) \Rightarrow f^{-1}(s) \text{ infinite}$$$

Lean4

protected theorem preimage (hs : s.Infinite) (hf : s ⊆ range f) : (f ⁻¹' s).Infinite := fun h ↦
  hs <| finite_of_finite_preimage h hf

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