fintypeBind'

Mathlib.Data.Set.Finite.Monad

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

← MathLib Explorer

English

Instance: if s is finite and f is a function with finite outputs, then s >>= f is finite.

Русский

Экземпляр: если s конечно и f(a) конечно для всех a, то s >>= f конечно.

LaTeX

$$Fintype (s >>= f)$$

Lean4

instance fintypeBind' {α β} [DecidableEq β] (s : Set α) [Fintype s] (f : α → Set β) [∀ a, Fintype (f a)] :
    Fintype (s >>= f) :=
  Set.fintypeBiUnion' s f

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

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

Разделы

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

Аффилиация

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