bind — Mathlib

English

If s is finite and every f a is finite, then the bind s >>= f is finite.

Русский

Если множество s конечное и для каждого элемента a ∈ s множество f a конечное, тогда связывание s с f финит.

LaTeX

$$$ \forall s : \mathrm{Set}\alpha, \mathrm{Finite}(s) \land (\forall a \in s, \mathrm{Finite}(f a)) \rightarrow \mathrm{Finite}(s \bind f)$$$

Lean4

theorem bind {α β} {s : Set α} {f : α → Set β} (h : s.Finite) (hf : ∀ a ∈ s, (f a).Finite) : (s >>= f).Finite :=
  h.biUnion hf

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