antivaryOn_iff_exists_antitoneOn_monotoneOn

English

For f: ι → α, g: ι → β and s ⊆ ι, AntivaryOn f g s holds iff there exists a linear order on ι under which f is antitone on s and monotone on g 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{AntitoneOn}(f,s) \wedge \mathrm{MonotoneOn}(g,s)$$$

Lean4

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

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