card_bind — Mathlib

English

The cardinality of the parts of P.bind Q equals the sum of the cardinalities of the parts of Q over P.parts.

Русский

Кардинал частей P.bind Q равен сумме кардиналов частей Q по каждому элементу P.parts.

LaTeX

$$ #(P.bind Q).parts = \sum_{A \in P.parts} #(Q A).parts $$

Lean4

theorem card_bind (Q : ∀ i ∈ P.parts, Finpartition i) : #(P.bind Q).parts = ∑ A ∈ P.parts.attach, #(Q _ A.2).parts :=
  by
  apply card_biUnion
  rintro ⟨b, hb⟩ - ⟨c, hc⟩ - hbc
  rw [Function.onFun, Finset.disjoint_left]
  rintro d hdb hdc
  rw [Ne, Subtype.mk_eq_mk] at hbc
  exact
    (Q b hb).ne_bot hdb
      (eq_bot_iff.2 <| (le_inf ((Q b hb).le hdb) <| (Q c hc).le hdc).trans <| (P.disjoint hb hc hbc).le_bot)

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