English
The predicate 𝒜.Shatters is a decidable predicate (for fixed α).
Русский
Предикат 𝒜.Shatters является разрешимым (для фиксированного α).
LaTeX
$$$ \text{DecidablePred } 𝒜.Shatters $$$
Lean4
/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements more than something in `𝒜`. -/
theorem mem_upShadow_iff_exists_mem_card_add : s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + k = #s := by
induction k generalizing 𝒜 s with
| zero =>
refine ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, ?_⟩
rintro ⟨t, ht, hst, hcard⟩
rwa [← eq_of_subset_of_card_le hst hcard.ge]
| succ k ih =>
simp only [Function.comp_apply, Function.iterate_succ]
refine ih.trans ?_
clear ih
constructor
· rintro ⟨t, ht, hts, hcardst⟩
obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
refine ⟨u, hu, hut.trans hts, ?_⟩
rw [← hcardst, hcardtu, add_right_comm]
rfl
· rintro ⟨t, ht, hts, hcard⟩
obtain ⟨u, htu, hus, hu⟩ := Finset.exists_subsuperset_card_eq hts (Nat.le_add_right _ 1) (by cutsat)
refine ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu⟩, hus, ?_⟩
rw [hu, ← hcard, add_right_comm]
rfl
