English
Let f: α → E and φ: β → α be monotone on t. For any x,y ∈ t, the variation of f ∘ φ on t ∩ Icc x y equals the variation of f on φ(t) ∩ Icc (φ x) (φ y): eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y)).
Русский
Пусть f: α → E и φ: β → α монотонны на t. Для любых x,y ∈ t велика вариация на t ∩ Icc(x,y) композиции f ∘ φ равна вариации на φ(t) ∩ Icc(φx)(φy): eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ'' t ∩ Icc (φ x) (φ y)).
LaTeX
$$$eVariationOn\\bigl(f \\circ \\phi\\bigr)\\bigl(t \\cap Icc\\,x\\,y\\bigr) = eVariationOn f\\bigl(\\phi''t \\cap Icc\\,\\bigl(\\phi x\\bigr)\\bigl(\\phi y\\bigr)\\bigr)$$$
Lean4
theorem comp_inter_Icc_eq_of_monotoneOn (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t)
(hy : y ∈ t) : eVariationOn (f ∘ φ) (t ∩ Icc x y) = eVariationOn f (φ '' t ∩ Icc (φ x) (φ y)) :=
by
rcases le_total x y with (h | h)
· convert comp_eq_of_monotoneOn f φ (hφ.mono Set.inter_subset_left)
apply le_antisymm
· rintro _ ⟨⟨u, us, rfl⟩, vφx, vφy⟩
rcases le_total x u with (xu | ux)
· rcases le_total u y with (uy | yu)
· exact ⟨u, ⟨us, ⟨xu, uy⟩⟩, rfl⟩
· rw [le_antisymm vφy (hφ hy us yu)]
exact ⟨y, ⟨hy, ⟨h, le_rfl⟩⟩, rfl⟩
· rw [← le_antisymm vφx (hφ us hx ux)]
exact ⟨x, ⟨hx, ⟨le_rfl, h⟩⟩, rfl⟩
· rintro _ ⟨u, ⟨⟨hu, xu, uy⟩, rfl⟩⟩
exact ⟨⟨u, hu, rfl⟩, ⟨hφ hx hu xu, hφ hu hy uy⟩⟩
· rw [eVariationOn.subsingleton, eVariationOn.subsingleton]
exacts [(Set.subsingleton_Icc_of_ge (hφ hy hx h)).anti Set.inter_subset_right,
(Set.subsingleton_Icc_of_ge h).anti Set.inter_subset_right]
