card_memberSubfamily_add_card_nonMemberSubfamily

English

The sum of the cardinalities of 𝒜.memberSubfamily a and 𝒜.nonMemberSubfamily a equals the cardinality of 𝒜.

Русский

Сумма кардинальностей 𝒜.memberSubfamily a и 𝒜.nonMemberSubfamily a равна кардинальности 𝒜.

LaTeX

$$$#(𝒜.\text{memberSubfamily} a) + #(𝒜.\text{nonMemberSubfamily} a) = #𝒜$$$

Lean4

theorem card_memberSubfamily_add_card_nonMemberSubfamily (a : α) (𝒜 : Finset (Finset α)) :
    #(𝒜.memberSubfamily a) + #(𝒜.nonMemberSubfamily a) = #𝒜 :=
  by
  rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
  · conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
  · apply (erase_injOn' _).mono
    simp

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