mem_upShadow_iterate_iff_exists_sdiff

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` is in the upper shadow of `𝒜` iff `t` is exactly `k` elements less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add`. -/
theorem mem_upShadow_iterate_iff_exists_sdiff : t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k :=
  by
  rw [mem_upShadow_iterate_iff_exists_card]
  constructor
  · rintro ⟨u, rfl, hut, htu⟩
    exact ⟨_, htu, sdiff_subset, by rw [sdiff_sdiff_eq_self hut]⟩
  · rintro ⟨s, hs, hst, rfl⟩
    exact ⟨_, rfl, sdiff_subset, by rwa [sdiff_sdiff_eq_self hst]⟩

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