English
If a ≤ b ≤ c and b ∈ s, then eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c).
Русский
Если a ≤ b ≤ c и b ∈ s, то V(s∩Icc(a,b)) + V(s∩Icc(b,c)) = V(s∩Icc(a,c)).
LaTeX
$$$a,b,c\in α,\; a\le b,\; b\le c,\; b\in s\Rightarrow eVariationOn f (s\cap Icc a b) + eVariationOn f (s\cap Icc b c) = eVariationOn f (s\cap Icc a c)$$
Lean4
theorem Icc_add_Icc (f : α → E) {s : Set α} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) (hb : b ∈ s) :
eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c) :=
by
have A : IsGreatest (s ∩ Icc a b) b := ⟨⟨hb, hab, le_rfl⟩, inter_subset_right.trans Icc_subset_Iic_self⟩
have B : IsLeast (s ∩ Icc b c) b := ⟨⟨hb, le_rfl, hbc⟩, inter_subset_right.trans Icc_subset_Ici_self⟩
rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]
