restrict_boxes_of_le — Mathlib

English

restrict_self states the equality π.restrict I = π.

Русский

restrict_self утверждает равенство π.restrict I = π.

LaTeX

$$$ \\text{restrict\_self}: \\; π.restrict I = π $$$

Lean4

/-- Restricting to a larger box does not change the set of boxes. We cannot claim equality
of prepartitions because they have different types. -/
theorem restrict_boxes_of_le (π : Prepartition I) (h : I ≤ J) : (π.restrict J).boxes = π.boxes := by
  classical
  simp only [restrict, ofWithBot, eraseNone_eq_biUnion]
  refine Finset.image_biUnion.trans ?_
  refine (Finset.biUnion_congr rfl ?_).trans Finset.biUnion_singleton_eq_self
  intro J' hJ'
  rw [inf_of_le_right, ← WithBot.some_eq_coe, Option.toFinset_some]
  exact WithBot.coe_le_coe.2 ((π.le_of_mem hJ').trans h)

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