antivaryOn_iff_exists_monotoneOn_antitoneOn

English

For f: ι → α, g: ι → β and s ⊆ ι, AntivaryOn f g s holds if and only if there exists a linear order on ι under which f is monotone on s and g is antitone on s.

Русский

Пусть f: ι → α, g: ι → β и s ⊆ ι. AntivaryOn f g s эквивалентно существованию линейного порядка на ι, при котором f монотонна на s, а g антитонна на s.

LaTeX

$$$\mathrm{AntivaryOn}(f,g,s) \iff \exists\,(L: \text{ LinearOrder } ι), \ \mathrm{MonotoneOn}(f,s) \wedge \mathrm{AntitoneOn}(g,s)$$$

Lean4

theorem antivaryOn_iff_exists_monotoneOn_antitoneOn :
    AntivaryOn f g s ↔ ∃ (_ : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s := by
  simp_rw [← monovaryOn_toDual_right, monovaryOn_iff_exists_monotoneOn, monotoneOn_toDual_comp_iff]

Похожие утверждения