English
A variant of the composition invariance for monotone φ on t, with roles reversed depending on the order relation between x and y.
Русский
Вариант инвариантности композиции для монотонного φ на t с учетом порядка между x и y.
LaTeX
$$variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)$$
Lean4
protected theorem comp_eq_of_monotoneOn {β : Type*} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α)
(hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) :
variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y) :=
by
rcases le_total x y with (h | h)
·
rw [variationOnFromTo.eq_of_le _ _ h, variationOnFromTo.eq_of_le _ _ (hφ hx hy h),
eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hx hy]
·
rw [variationOnFromTo.eq_of_ge _ _ h, variationOnFromTo.eq_of_ge _ _ (hφ hy hx h),
eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hy hx]
