antivary_iff_exists_antitone_monotone

English

For f: ι → α, g: ι → β and s ⊆ ι, Antivary f g holds iff there exists a linear order on ι under which anticorresponding monotonicity holds between f and g.

Русский

Для f: ι → α, g: ι → β и s ⊆ ι, Antivary f g сохраняется тогда, когда существует линейный порядок на ι, обеспечивающий требуемую зависимость монотонности между f и g.

LaTeX

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

Lean4

theorem antivary_iff_exists_antitone_monotone : Antivary f g ↔ ∃ (_ : LinearOrder ι), Antitone f ∧ Monotone g := by
  simp [← antivaryOn_univ, antivaryOn_iff_exists_antitoneOn_monotoneOn]

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