fintypeSeq' — Mathlib

English

If F is a finite set of functions from α to β and S is a finite subset of α, then the applicative product F <*> S is finite.

Русский

Если F — конечное множество функций из α в β, а S — конечное подмножество α, то F <*> S конечное.

LaTeX

$$$ \forall f : \mathrm{Set}(\alpha \to \beta), \forall s : \mathrm{Set}\alpha, \mathrm{Finite}(f) \land \mathrm{Finite}(s) \rightarrow \mathrm{Finite}(f \,<*>\, s)$$$

Lean4

instance fintypeSeq' {α β : Type u} [DecidableEq β] (f : Set (α → β)) (s : Set α) [Fintype f] [Fintype s] :
    Fintype (f <*> s) :=
  Set.fintypeSeq f s

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