card_le_diff_of_interleaved — Mathlib

English

If s and t are interleaved, then card(s) ≤ card(t \\ s) + 1.

Русский

Если s и t чередуются, то размер s не превосходит размер множества t \ s плюс 1.

LaTeX

$$$ |s| \\le |t \\setminus s| + 1 $$$

Lean4

/-- If finsets `s` and `t` are interleaved, then `Finset.card s ≤ Finset.card (t \ s) + 1`. -/
theorem card_le_diff_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 \ s).card + 1 :=
  card_le_of_interleaved fun x hx y hy hxy hs =>
    let ⟨z, hzt, hxz, hzy⟩ := h x hx y hy hxy hs
    ⟨z, mem_sdiff.2 ⟨hzt, fun hzs => hs z hzs ⟨hxz, hzy⟩⟩, hxz, hzy⟩

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