prepartition_isSubordinate — Mathlib

English

If B is a box and r > 0 with 1/n ≤ r, then the prepartition n B is subordinate to the gauge mapping every point to the box ⟨r, with r positive⟩.

Русский

Если B — коробка и r > 0 с условием 1/n ≤ r, то разбиение prepartition n B подпорядковано функции градаций, которая каждому моменту сопоставляет коробку с параметром r.

LaTeX

$$$$ (\mathrm{prepartition}(n,B)).\mathrm{IsSubordinate}\bigl(\lambda\_\mapsto \langle r,\, hr\rangle\bigr). $$$$

Lean4

theorem prepartition_isSubordinate (B : Box ι) {r : ℝ} (hr : 0 < r) (hn : 1 / n ≤ r) :
    (prepartition n B).IsSubordinate (fun _ ↦ ⟨r, hr⟩) :=
  by
  intro _ hI
  obtain ⟨ν, hν, rfl⟩ := mem_prepartition_iff.mp hI
  refine fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_
  · rw [prepartition_tag n hν]
    exact Box.coe_subset_Icc (tag_mem _ _)
  · exact le_trans (diam_boxIcc n ν) hn

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