instFintype — Mathlib

English

The set of RelEmbedding between two relations on finite types is finite.

Русский

Набор RelEmbedding между отношениями на конечных типах конечно.

LaTeX

$$$\\text{Fintype}(\\text{RelEmbedding } r s)$ is finite.$$

Lean4

noncomputable instance instFintype {α β} [Fintype α] [Fintype β] {r : α → α → Prop} {s : β → β → Prop} :
    Fintype (r ↪r s) :=
  Fintype.ofInjective _ RelEmbedding.toEmbedding_injective

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