antivary_iff_exists_monotone_antitone

English

For f: ι → α, g: ι → β and s ⊆ ι, AntivaryOn f g s holds iff 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 antivary_iff_exists_monotone_antitone : Antivary f g ↔ ∃ (_ : LinearOrder ι), Monotone f ∧ Antitone g := by
  simp [← antivaryOn_univ, antivaryOn_iff_exists_monotoneOn_antitoneOn]

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