English
For f: ι → α, g: ι → β and s ⊆ ι, MonovaryOn f g s holds if and only if there exists a linear order on ι under which f and g are both monotone on s.
Русский
Для функций f: ι → α, g: ι → β и множества s ⊆ ι, MonovaryOn f g s эквивалентно существованию линейного порядка на ι, при котором и f, и g монотонны на s.
LaTeX
$$$\mathrm{MonovaryOn}(f,g,s) \iff \exists\,(L: \text{LinearOrder } ι), \ \mathrm{MonotoneOn}(f,s) \wedge \mathrm{MonotoneOn}(g,s)$$$
Lean4
theorem monovaryOn_iff_exists_monotoneOn : MonovaryOn f g s ↔ ∃ (_ : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s :=
by
classical
letI := linearOrderOfSTO (MonovaryOrder f g)
refine
⟨fun hfg =>
⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
· obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
· obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
· exact hfg.symm hi hj h
obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
· rintro ⟨_, hf, hg⟩
exact hf.monovaryOn hg
