mem_shadow_iterate_iff_exists_sdiff

English

t ∈ ∂^[k] 𝒜 iff ∃ s ∈ 𝒜 with t ⊆ s and |s| = |t| + k.

Русский

t принадлежит ∂^[k] 𝒜 тогда и только тогда, когда существует s ∈ 𝒜 такое, что t ⊆ s и |s| = |t| + k.

LaTeX

$$$$ t \\in ∂^{[k]} 𝒜 \\iff \\exists s \\in 𝒜, t \\subseteq s \\land |s| = |t| + k $$$$

Lean4

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

See also `Finset.mem_shadow_iff_exists_mem_card_add`. -/
theorem mem_shadow_iterate_iff_exists_sdiff : t ∈ ∂ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k :=
  by
  rw [mem_shadow_iterate_iff_exists_card]
  constructor
  · rintro ⟨u, rfl, htu, hsuA⟩
    exact ⟨_, hsuA, subset_union_left, by rw [union_sdiff_cancel_left htu]⟩
  · rintro ⟨s, hs, hts, rfl⟩
    refine ⟨s \ t, rfl, disjoint_sdiff, ?_⟩
    rwa [union_sdiff_self_eq_union, union_eq_right.2 hts]

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