finite — Mathlib

English

The set of all embeddings α ↪ β is finite whenever β is finite.

Русский

Множество вложений (инъекций) α в β конечно при конечности β.

LaTeX

$$$ \\text{Finite }\\beta \\Rightarrow \\text{Finite}(\\text{Embedding }(\\alpha,\\beta)) $$$

Lean4

instance finite {α β : Sort*} [Finite β] : Finite (α ↪ β) :=
  by
  rcases isEmpty_or_nonempty (α ↪ β) with _ | h
  · infer_instance
  · refine h.elim fun f => ?_
    haveI : Finite α := Finite.of_injective _ f.injective
    exact Finite.of_injective _ DFunLike.coe_injective

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