instFintype — Mathlib

English

The collection of RelHom between two relations on finite types is finite.

Русский

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

LaTeX

$$$\\text{Fintype}(\\,r \\to_r s\\,)$ where $r,s$ are relations on finite types is finite.$$

Lean4

instance instFintype {α β} [Fintype α] [Fintype β] [DecidableEq α] {r : α → α → Prop} {s : β → β → Prop}
    [DecidableRel r] [DecidableRel s] : Fintype (r →r s) :=
  Fintype.ofEquiv { f : α → β // ∀ {x y}, r x y → s (f x) (f y) } <|
    Equiv.mk (fun f ↦ ⟨f.1, f.2⟩) (fun f ↦ ⟨f.1, f.2⟩) (fun _ ↦ rfl) (fun _ ↦ rfl)

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