Documentation

Mathlib.Order.Monotone.MonovaryOrder

Interpreting monovarying functions as monotone functions #

This file proves that monovarying functions to linear orders can be made simultaneously monotone by setting the correct order on their shared indexing type.

source
def MonovaryOrder {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] (f : ι → α) (g : ι → β) (i j : ι) :
Prop

If f : ι → α and g : ι → β are monovarying, then MonovaryOrder f g is a linear order on ι that makes f and g simultaneously monotone. We define i < j if f i < f j, or if f i = f j and g i < g j, breaking ties arbitrarily.

Equations
Instances For
    source
    instance instIsStrictTotalOrderMonovaryOrder {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] (f : ι → α) (g : ι → β) :
    IsStrictTotalOrder ι (MonovaryOrder f g)
    source
    theorem monovaryOn_iff_exists_monotoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s
    source
    theorem antivaryOn_iff_exists_monotoneOn_antitoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s
    source
    theorem monovaryOn_iff_exists_antitoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    MonovaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s
    source
    theorem antivaryOn_iff_exists_antitoneOn_monotoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    AntivaryOn f g s ↔ ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s
    source
    theorem monovary_iff_exists_monotone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Monovary f g ↔ ∃ (x : LinearOrder ι), Monotone f ∧ Monotone g
    source
    theorem monovary_iff_exists_antitone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Monovary f g ↔ ∃ (x : LinearOrder ι), Antitone f ∧ Antitone g
    source
    theorem antivary_iff_exists_monotone_antitone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Antivary f g ↔ ∃ (x : LinearOrder ι), Monotone f ∧ Antitone g
    source
    theorem antivary_iff_exists_antitone_monotone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Antivary f g ↔ ∃ (x : LinearOrder ι), Antitone f ∧ Monotone g
    source
    theorem MonovaryOn.exists_monotoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    MonovaryOn f g s → ∃ (x : LinearOrder ι), MonotoneOn f s ∧ MonotoneOn g s

    Alias of the forward direction of monovaryOn_iff_exists_monotoneOn.

    source
    theorem MonovaryOn.exists_antitoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    MonovaryOn f g s → ∃ (x : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s

    Alias of the forward direction of monovaryOn_iff_exists_antitoneOn.

    source
    theorem AntivaryOn.exists_monotoneOn_antitoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    AntivaryOn f g s → ∃ (x : LinearOrder ι), MonotoneOn f s ∧ AntitoneOn g s

    Alias of the forward direction of antivaryOn_iff_exists_monotoneOn_antitoneOn.

    source
    theorem AntivaryOn.exists_antitoneOn_monotoneOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :
    AntivaryOn f g s → ∃ (x : LinearOrder ι), AntitoneOn f s ∧ MonotoneOn g s

    Alias of the forward direction of antivaryOn_iff_exists_antitoneOn_monotoneOn.

    source
    theorem Monovary.exists_monotone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Monovary f g → ∃ (x : LinearOrder ι), Monotone f ∧ Monotone g

    Alias of the forward direction of monovary_iff_exists_monotone.

    source
    theorem Monovary.exists_antitone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Monovary f g → ∃ (x : LinearOrder ι), Antitone f ∧ Antitone g

    Alias of the forward direction of monovary_iff_exists_antitone.

    source
    theorem Antivary.exists_monotone_antitone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Antivary f g → ∃ (x : LinearOrder ι), Monotone f ∧ Antitone g

    Alias of the forward direction of antivary_iff_exists_monotone_antitone.

    source
    theorem Antivary.exists_antitone_monotone {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :
    Antivary f g → ∃ (x : LinearOrder ι), Antitone f ∧ Monotone g

    Alias of the forward direction of antivary_iff_exists_antitone_monotone.