map_split_add — Mathlib

English

Splitting along a coordinate and adding the resulting pieces recovers the original value of the map.

Русский

Разделение по координате и сложение частей восстанавливают исходное значение отображения.

LaTeX

$$$ (I.splitLower i x).elim'0 f + (I.splitUpper i x).elim'0 f = f(I)$$$

Lean4

@[simp]
theorem map_split_add (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) (i : ι) (x : ℝ) :
    (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f = f I := by
  rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]

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