mem_shadow_iterate_iff_exists_mem_card_add

English

The shadow of a family of r-sets is a family of (r−1)-sets.

Русский

Тень семейства r-множест̧в — это семейство множеств размером (r−1).

LaTeX

$$$$ \\partial 𝒜 : \\text{Размер} = r-1 \\text{ если } 𝒜 : \\text{Размер} = r $$$$

Lean4

/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something in `𝒜`.

See also `Finset.mem_shadow_iterate_iff_exists_sdiff`. -/
theorem mem_shadow_iterate_iff_exists_mem_card_add : t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + k :=
  by
  refine
    mem_shadow_iterate_iff_exists_sdiff.trans <|
      exists_congr fun t ↦ and_congr_right fun _ ↦ and_congr_right fun hst ↦ ?_
  rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
  exact card_mono hst

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