English
If finite sets s and t are interleaved in a linear order, then card(s) ≤ card(t) + 1.
Русский
Если конечные множества s и t чередуются в линейном порядке, тогда размер s не превосходит размер t плюс 1.
LaTeX
$$$ |s| \\le |t| + 1 \\quad\\text{under interleaving condition}$$$
Lean4
/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card t + 1`. -/
theorem card_le_of_interleaved {s t : Finset α}
(h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) : s.card ≤ t.card + 1 :=
by
replace h : ∀ᵉ (x ∈ s) (y ∈ s), x < y → ∃ z ∈ t, x < z ∧ z < y :=
by
intro x hx y hy hxy
rcases exists_next_right ⟨y, hy, hxy⟩ with ⟨a, has, hxa, ha⟩
rcases h x hx a has hxa fun z hzs hz => hz.2.not_ge <| ha _ hzs hz.1 with ⟨b, hbt, hxb, hba⟩
exact ⟨b, hbt, hxb, hba.trans_le <| ha _ hy hxy⟩
set f : α → WithTop α := fun x => (t.filter fun y => x < y).min
have f_mono : StrictMonoOn f s := by
intro x hx y hy hxy
rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
calc
f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
_ < f y :=
(Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)
calc
s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
_ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
(card_mono <|
image_subset_iff.2 fun x _ =>
insert_subset_insert _ (image_subset_image <| filter_subset _ _) (min_mem_insert_top_image_coe _))
_ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)
