finite — Mathlib

English

If α is finite and each β(i) is finite, then F is finite.

Русский

Если α конечно, и каждый β(i) конечно, то F конечно.

LaTeX

$$$[Finite\ α] [\forall i, Finite(β(i))] \Rightarrow Finite F$$$

Lean4

/-- All `DFunLike`s are finite if their domain and codomain are.

Can't be an instance because it can cause infinite loops.
-/
theorem finite [Finite α] [∀ i, Finite (β i)] : Finite F :=
  Finite.of_injective _ DFunLike.coe_injective

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