hall_cond_of_erase — Mathlib

English

If the Hall condition holds on ι, then after removing a fixed element a from a single t(i) we still have a Hall-type bound for the restricted family.

Русский

Если условие Холла выполняется на ι, то после удаления фиксированного элемента a из каждого t(i) для i в рассматриваемой подмножности сохраняется подобное ограничение Холла.

LaTeX

$$$\\\\forall a, \\\\text{Hall }(t) \\\\Rightarrow \\\\forall s, |s| \\\\le |\\\\bigcup_{i\\\\in s} (t(i) \\\\setminus \\{a\\\\})|.$$$

Lean4

theorem hall_cond_of_erase {x : ι} (a : α) (ha : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t))
    (s' : Finset {x' : ι | x' ≠ x}) : #s' ≤ #(s'.biUnion fun x' => (t x').erase a) :=
  by
  haveI := Classical.decEq ι
  specialize ha (s'.image fun z => z.1)
  rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha
  by_cases he : s'.Nonempty
  · have ha' : #s' < #(s'.biUnion fun x => t x) :=
      by
      convert ha he fun h => by simpa [← h] using mem_univ x using 2
      ext x
      simp only [mem_image, mem_biUnion, SetCoe.exists, exists_and_right, exists_eq_right]
    rw [← erase_biUnion]
    by_cases hb : a ∈ s'.biUnion fun x => t x
    · rw [card_erase_of_mem hb]
      exact Nat.le_sub_one_of_lt ha'
    · rw [erase_eq_of_notMem hb]
      exact Nat.le_of_lt ha'
  · rw [nonempty_iff_ne_empty, not_not] at he
    subst s'
    simp

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