card_filter_tag_eq_le — Mathlib

English

In a Henstock prepartition, for each fixed tag x, the number of boxes with that tag is at most 2^{|ι|}.

Русский

В гентской предразбиении число коробок с фиксированной меткой x не превосходит 2^{|ι|}.

LaTeX

$$$$ \\#\\{J \\in \\pi.boxes \\mid \\pi.tag J = x\\} \\le 2^{|\\iota|} $$$$

Lean4

/-- In a Henstock prepartition, there are at most `2 ^ Fintype.card ι` boxes with a given tag. -/
theorem card_filter_tag_eq_le [Fintype ι] (h : π.IsHenstock) (x : ι → ℝ) :
    #({J ∈ π.boxes | π.tag J = x}) ≤ 2 ^ Fintype.card ι := by
  classical
    calc
    #({J ∈ π.boxes | π.tag J = x}) ≤ #({J ∈ π.boxes | x ∈ Box.Icc J}) :=
      by
      refine Finset.card_le_card fun J hJ => ?_
      rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
      exact ⟨hJ, h J hJ⟩
    _ ≤ 2 ^ Fintype.card ι := π.toPrepartition.card_filter_mem_Icc_le x

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