English
If the compression of 𝒜 along a is a shatters s, then 𝒜 shatters s as well.
Русский
Если сжатие 𝒜 по a шаттерит s, то и 𝒜 шаттерит s.
LaTeX
$$$ (Down.compression\\ a\\ 𝒜).Shatters\\ s \\Rightarrow 𝒜.Shatters s $$$
Lean4
theorem of_compression (hs : (𝓓 a 𝒜).Shatters s) : 𝒜.Shatters s :=
by
intro t ht
obtain ⟨u, hu, rfl⟩ := hs ht
rw [Down.mem_compression] at hu
obtain hu | hu := hu
· exact ⟨u, hu.1, rfl⟩
by_cases ha : a ∈ s
· obtain ⟨v, hv, hsv⟩ := hs <| insert_subset ha ht
rw [Down.mem_compression] at hv
obtain hv | hv := hv
· refine ⟨erase v a, hv.2, ?_⟩
rw [inter_erase, hsv, erase_insert]
rintro ha
rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
exact hu.1 hu.2
rw [insert_eq_self.2 <| inter_subset_right (s₁ := s) ?_] at hv
cases hv.1 hv.2
rw [hsv]
exact mem_insert_self _ _
· refine ⟨insert a u, hu.2, ?_⟩
rw [inter_insert_of_notMem ha]
