card_bind — Mathlib

English

The cardinal of a bind equals the sum of the cardinalities of the inner images: card (s.bind f) = (s.map (card ∘ f)).sum.

Русский

Кардинал связывания равен сумме кардиналов образов: card (s.bind f) = (s.map (card ∘ f)).sum.

LaTeX

$$$\\mathrm{card}(\\mathrm{bind}\\, f\\, S) = (\\mathrm{map}\\ (\\mathrm{card} \\circ f)\\, S).\\mathrm{sum}$$$

Lean4

@[simp]
theorem card_bind : card (s.bind f) = (s.map (card ∘ f)).sum := by simp [bind]

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