card_le_card_biUnion_add_one — Mathlib

English

If f is injective and the s elements are pairwise disjoint, then |s| ≤ |s.biUnion f| + 1.

Русский

Если f инъективна и элементы s попарно непересекаются, то |s| ≤ |s.biUnion f| + 1.

LaTeX

$$$\\text{If } f \\text{ injective and } s. toSet. PairwiseDisjoint f, \\; |s| ≤ |s.biUnion f| + 1$$$

Lean4

theorem card_le_card_biUnion_add_one {s : Finset ι} {f : ι → Finset α} (hf : Injective f)
    (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1 :=
  (card_le_card_biUnion_add_card_fiber hs).trans <|
    add_le_add_left (card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm) _

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