fintypeBind — Mathlib

English

If s has a Fintype instance and f(a) is finite for all a ∈ s, then the dependent union s >>= f is finite.

Русский

Если у s есть экземпляр Fintype, и для каждого a ∈ s множество f(a) конечно, то объединение s >>= f конечно.

LaTeX

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

Lean4

/-- If `s : Set α` is a set with `Fintype` instance and `f : α → Set β` is a function such that
each `f a`, `a ∈ s`, has a `Fintype` structure, then `s >>= f` has a `Fintype` structure. -/
def fintypeBind {α β} [DecidableEq β] (s : Set α) [Fintype s] (f : α → Set β) (H : ∀ a ∈ s, Fintype (f a)) :
    Fintype (s >>= f) :=
  Set.fintypeBiUnion s f H

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