card_filter_mem_Icc_le — Mathlib

English

The number of boxes in π.boxes for which x lies in the closed box is bounded by 2^{card ι}.

Русский

Число коробок из π.boxes, в которых x лежит в закрытом интервалe, не превосходит 2^{card ι}.

LaTeX

$$$\#\{ J \in π.boxes \mid x \in Box.Icc(J) \} \le 2^{Fintype.card ι}$$$

Lean4

/-- The set of boxes of a prepartition that contain `x` in their closures has cardinality
at most `2 ^ Fintype.card ι`. -/
theorem card_filter_mem_Icc_le [Fintype ι] (x : ι → ℝ) : #({J ∈ π.boxes | x ∈ Box.Icc J}) ≤ 2 ^ Fintype.card ι :=
  by
  rw [← Fintype.card_set]
  refine Finset.card_le_card_of_injOn (fun J : Box ι => {i | J.lower i = x i}) (fun _ _ => Finset.mem_univ _) ?_
  simpa using π.injOn_setOf_mem_Icc_setOf_lower_eq x

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