English
The coercion from BoxAdditiveMap to functions is injective.
Русский
Коэрция BoxAdditiveMap в функции инъективна.
LaTeX
$$$\text{Injective }(f \mapsto f)$$$
Lean4
/-- If `f : Box ι → M` is box additive on partitions of the form `split I i x`, then it is box
additive. -/
def ofMapSplitAdd [Finite ι] (f : Box ι → M) (I₀ : WithTop (Box ι))
(hf :
∀ I : Box ι,
↑I ≤ I₀ →
∀ {i x},
x ∈ Ioo (I.lower i) (I.upper i) → (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f = f I) :
ι →ᵇᵃ[I₀] M := by
classical
refine ⟨f, ?_⟩
replace hf (I : Box ι) (hI : ↑I ≤ I₀) (s) : ∑ J ∈ (splitMany I s).boxes, f J = f I := by
induction s using Finset.induction_on with
| empty => simp
| insert a s _ ihs =>
rw [splitMany_insert, inf_split, ← ihs, biUnion_boxes, sum_biUnion_boxes]
refine Finset.sum_congr rfl fun J' hJ' => ?_
by_cases h : a.2 ∈ Ioo (J'.lower a.1) (J'.upper a.1)
· rw [sum_split_boxes]
exact hf _ ((WithTop.coe_le_coe.2 <| le_of_mem _ hJ').trans hI) h
· rw [split_of_notMem_Ioo h, top_boxes, Finset.sum_singleton]
intro I hI π hπ
have Hle : ∀ J ∈ π, ↑J ≤ I₀ := fun J hJ => (WithTop.coe_le_coe.2 <| π.le_of_mem hJ).trans hI
rcases hπ.exists_splitMany_le with ⟨s, hs⟩
rw [← hf _ hI, ← inf_of_le_right hs, inf_splitMany, biUnion_boxes, sum_biUnion_boxes]
exact Finset.sum_congr rfl fun J hJ => (hf _ (Hle _ hJ) _).symm
