fintypeSeq — Mathlib

English

If f ⊆ Set (α → β) is finite and s ⊆ Set α is finite, then the sequence set f.seq s is finite.

Русский

Если f — конечное множество функций α → β, и s ⊆ Set α — конечен, то множество последовательностей f.seq s конечно.

LaTeX

$$Fintype (f.seq s).Elem$$

Lean4

instance fintypeSeq [DecidableEq β] (f : Set (α → β)) (s : Set α) [Fintype f] [Fintype s] : Fintype (f.seq s) :=
  by
  rw [seq_def]
  apply Set.fintypeBiUnion'

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