card_le_card_biUnion_add_card_fiber

English

For s, f, with hs pairwise disjoint, we have |s| ≤ |s.biUnion f| + |{i ∈ s | f i = ∅}|.

Русский

Пусть s, f образуют попарно непересекающиеся семейства; тогда |s| ≤ |s.biUnion f| + |{i ∈ s | f i = ∅}|.

LaTeX

$$$#s ≤ #(s. biUnion f) + #\\{i ∈ s \\mid f i = ∅\\}$$$

Lean4

theorem card_le_card_biUnion_add_card_fiber {s : Finset ι} {f : ι → Finset α} (hs : (s : Set ι).PairwiseDisjoint f) :
    #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅}) :=
  by
  rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]
  exact
    add_le_add_right
      ((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
            nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
        card_le_card <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
      _

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