finite_seq — Mathlib

English

If F is a finite set of functions and S is a finite set, then F.seq S is finite.

Русский

Если F — конечное множество функций, а S — конечное множество, то F.seq 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.\mathrm{seq}~s)$$$

Lean4

instance finite_seq (f : Set (α → β)) (s : Set α) [Finite f] [Finite s] : Finite (f.seq s) :=
  by
  rw [seq_def]
  infer_instance

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