restrict_split — Mathlib

English

If I ≤ J, then restricting the split of J to I yields the split of I: (split J i x).restrict I = split I i x.

Русский

Если I ⊆ J, ограничение разбиения split J i x до I дает разбиение split I i x.

LaTeX

$$$\\big(\\mathrm{split}\\ J\\ i\\ x\\big).\\mathrm{restrict}\\ I = \\mathrm{split}\\ I\\ i\\ x$$$

Lean4

@[simp]
theorem restrict_split (h : I ≤ J) (i : ι) (x : ℝ) : (split J i x).restrict I = split I i x :=
  by
  refine ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset ?_
  simp only [Finset.subset_iff, mem_boxes, mem_restrict', mem_split_iff']
  have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => inter_subset_left.trans h
  rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left; right] <;> simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]

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