seq'

Mathlib.Data.Set.Finite.Monad

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

← MathLib Explorer

English

The same finiteness result as above, for the variant seq'.

Русский

Та же конченность для варианта seq'.

LaTeX

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

Lean4

theorem seq' {α β : Type u} {f : Set (α → β)} {s : Set α} (hf : f.Finite) (hs : s.Finite) : (f <*> s).Finite :=
  hf.seq hs

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

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

Разделы

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

Аффилиация

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