seq

Mathlib.Data.Set.Finite.Monad

URI: https://scilib.ai/kg/mathlib#Set.Finite.seq

← MathLib Explorer

English

If f and s are finite, 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

theorem seq {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f.seq s).Finite :=
  hf.image2 _ hs

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru