English
If φ is monotone on t, ψ is a right inverse of φ on s, and ψ maps s into t, then ψ is monotone on s.
Русский
Если φ монотонна на t, ψ является правым обратным к φ на s, и ψ отображает s в t, то ψ монотонна на s.
LaTeX
$$$\operatorname{MonotoneOn}(\varphi,t) \to \operatorname{RightInvOn}(\psi,\varphi,s) \to \operatorname{MapsTo}(\psi,s,t) \Rightarrow \operatorname{MonotoneOn}(\psi,s)$$$
Lean4
theorem monotoneOn_of_rightInvOn_of_mapsTo {α β : Type*} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β}
{t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :
MonotoneOn ψ s := by
rintro x xs y ys l
rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)
· exact ψxy
· have := hφ (ψts ys) (ψts xs) ψyx
rw [φψs.eq ys, φψs.eq xs] at this
induction le_antisymm l this
exact le_refl _
