powersetCard_sup — Mathlib

English

Let u be a finite set and n a natural number with n < |u|. Then the union of all (n+1)-element subsets of u is exactly u.

Русский

Пусть u — конечное множество и n — натуральное число such that n < |u|. Тогда объединение всех подмножеств u размером n+1 равно самому u.

LaTeX

$$$$\\text{If } u \\text{ is finite and } n < |u|,\\quad \\bigcup_{S \\subseteq u,\\ |S|=n+1} S = u.$$$$

Lean4

theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) :
    (powersetCard n.succ u).sup id = u := by
  apply le_antisymm
  · simp_rw [Finset.sup_le_iff, mem_powersetCard]
    rintro x ⟨h, -⟩
    exact h
  · rw [sup_eq_biUnion, le_iff_subset, subset_iff]
    intro x hx
    simp only [mem_biUnion, id]
    obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) :=
      powersetCard_nonempty.2 (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
    refine ⟨insert x t, ?_, mem_insert_self _ _⟩
    rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]
    exact mem_union_right _ (mem_image_of_mem _ ht)

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