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.