preimage' — Mathlib

English

If s is finite and each fiber of f over singleton sets inside s is finite, then the preimage f^{-1}(s) is finite.

Русский

Если s конечно и каждое пересечение f^{-1}({b}) с s конечно, то f^{-1}(s) конечно.

LaTeX

$$$\\operatorname{Finite}(s) \\rightarrow (\\forall b \\in s, (f^{-1} \\{b\\}).Finite) \\rightarrow (f^{-1}(s)).Finite$$$

Lean4

theorem preimage' (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' { b }).Finite) : (f ⁻¹' s).Finite :=
  by
  rw [← Set.biUnion_preimage_singleton]
  exact Set.Finite.biUnion h hf

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