instFintype — Mathlib

English

If B is finite, then A is finite, given SetLike A B and a finite B with an injection from A into B.

Русский

Если B конечен, то A конечен, если A имеет SetLike-структуру в B и имеется инъекция A → B.

LaTeX

$$$ \text{Finite}(B) \Rightarrow \text{Finite}(A) $$$

Lean4

/-- TODO: It should be possible to obtain a computable version of this for most
SetLike objects. If we add those instances, we should remove this one. -/
noncomputable instance (priority := 100) {A B : Type*} [SetLike A B] [Fintype B] : Fintype A :=
  Fintype.ofInjective SetLike.coe SetLike.coe_injective

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