English
A simplified version of the shadow-interaction with InitSeg.
Русский
Упрощенная версия взаимодействия тени и InitSeg.
LaTeX
$$$\text{ShadowInitSeg}(\mathcal{A})$ describes a simple isInitSeg relation$$
Lean4
/-- If we're compressed by all useful compressions, then we're an initial segment. This is the other
key Kruskal-Katona part. -/
theorem isInitSeg_of_compressed {ℬ : Finset (Finset α)} {r : ℕ} (h₁ : (ℬ : Set (Finset α)).Sized r)
(h₂ : ∀ U V, UsefulCompression U V → IsCompressed U V ℬ) : IsInitSeg ℬ r :=
by
refine ⟨h₁, ?_⟩
rintro A B hA ⟨hBA, sizeA⟩
by_contra hB
have hAB : A ≠ B := ne_of_mem_of_not_mem hA hB
have hAB' : #A = #B := (h₁ hA).trans sizeA.symm
have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB <| eq_of_subset_of_card_le h hAB'.ge
have hV : (B \ A).Nonempty := sdiff_nonempty.2 fun h ↦ hAB.symm <| eq_of_subset_of_card_le h hAB'.le
have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
have smaller : max' _ hV < max' _ hU :=
by
obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
· rw [← compress_sdiff_sdiff A B] at hAB hBA
cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB
· exact (disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim
· assumption
refine hB ?_
rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)
