mem_upShadow_iterate_iff_exists_mem_card_add

English

t ∈ ∂⁺^k 𝒜 iff ∃ s ∈ 𝒜, s ⊆ t ∧ |t| = |s| + k.

Русский

t ∈ ∂⁺^k 𝒜 тогда и только тогда, когда ∃ s ∈ 𝒜, s ⊆ t и |t| = |s| + k.

LaTeX

$$$ t ∈ ∂⁺^k 𝒜 \iff ∃ s ∈ 𝒜, s ⊆ t ∧ \#t = \#s + k $$$

Lean4

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

See also `Finset.mem_upShadow_iterate_iff_exists_sdiff`. -/
theorem mem_upShadow_iterate_iff_exists_mem_card_add : t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k :=
  by
  refine
    mem_upShadow_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

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