of_injective_finite_range — Mathlib

English

If α is finite and β(a) is finite for every a ∈ α, then the dependent sum Σ' a, β a is finite.

Русский

Если α конечно и для каждого a ∈ α множество β(a) конечно, то зависимое суммирование Σ'a, β a конечно.

LaTeX

$$$ [Finite α] \Rightarrow [\forall a, Finite (β a)] \Rightarrow Finite (\Sigma' a, β a) $$$

Lean4

theorem of_injective_finite_range {f : ι → α} (hf : Function.Injective f) [Finite (range f)] : Finite ι :=
  Finite.of_injective (Set.rangeFactorization f) (hf.codRestrict _)

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