Monotone functions over sets

Congruence lemmas for monotonicity and antitonicity

theorem MonotoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : MonotoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) : MonotoneOn f₂ s

theorem AntitoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : AntitoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) : AntitoneOn f₂ s

theorem StrictMonoOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : StrictMonoOn f₁ s) (h : Set.EqOn f₁ f₂ s) : StrictMonoOn f₂ s

theorem StrictAntiOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h₁ : StrictAntiOn f₁ s) (h : Set.EqOn f₁ f₂ s) : StrictAntiOn f₂ s

theorem Set.EqOn.congr_monotoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : EqOn f₁ f₂ s) : MonotoneOn f₁ s ↔ MonotoneOn f₂ s

theorem Set.EqOn.congr_antitoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : EqOn f₁ f₂ s) : AntitoneOn f₁ s ↔ AntitoneOn f₂ s

theorem Set.EqOn.congr_strictMonoOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : EqOn f₁ f₂ s) : StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s

theorem Set.EqOn.congr_strictAntiOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [Preorder α] [Preorder β] (h : EqOn f₁ f₂ s) : StrictAntiOn f₁ s ↔ StrictAntiOn f₂ s

Monotonicity lemmas

theorem MonotoneOn.mono {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂

theorem AntitoneOn.mono {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : AntitoneOn f s) (h' : s₂ ⊆ s) : AntitoneOn f s₂

theorem StrictMonoOn.mono {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictMonoOn f s) (h' : s₂ ⊆ s) : StrictMonoOn f s₂

theorem StrictAntiOn.mono {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictAntiOn f s) (h' : s₂ ⊆ s) : StrictAntiOn f s₂

theorem MonotoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : MonotoneOn f s) : Monotone (f ∘ Subtype.val)

theorem AntitoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : AntitoneOn f s) : Antitone (f ∘ Subtype.val)

theorem StrictMonoOn.strictMono {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictMonoOn f s) : StrictMono (f ∘ Subtype.val)

theorem StrictAntiOn.strictAnti {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] (h : StrictAntiOn f s) : StrictAnti (f ∘ Subtype.val)

theorem Set.monotoneOn_insert_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] {a : α} : MonotoneOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b ≤ a → f b ≤ f a) ∧ (∀ (b : α), b ∈ s → a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

theorem Set.antitoneOn_insert_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [Preorder α] [Preorder β] {a : α} : AntitoneOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b ≤ a → f a ≤ f b) ∧ (∀ (b : α), b ∈ s → a ≤ b → f b ≤ f a) ∧ AntitoneOn f s

Monotone

theorem Monotone.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : Monotone f) (s : Set α) : Monotone (s.restrict f)

theorem Monotone.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : Monotone f) {s : Set β} (hs : ∀ (x : α), f x ∈ s) : Monotone (Set.codRestrict f s hs)

theorem Monotone.rangeFactorization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : Monotone f) : Monotone (Set.rangeFactorization f)

@[simp]

theorem strictMono_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.restrict f) ↔ StrictMonoOn f s

theorem StrictMono.of_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMono (s.restrict f) → StrictMonoOn f s

Alias of the forward direction of strictMono_restrict.

theorem StrictMonoOn.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} : StrictMonoOn f s → StrictMono (s.restrict f)

Alias of the reverse direction of strictMono_restrict.

theorem StrictMono.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : StrictMono f) {s : Set β} (hs : ∀ (x : α), f x ∈ s) : StrictMono (Set.codRestrict f s hs)

theorem strictMonoOn_insert_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} : StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

theorem strictAntiOn_insert_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} : StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

theorem strictMonoOn_insert_iff_of_forall_le {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ (x : α), x ∈ s → x ≤ a) : StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s

theorem strictMonoOn_insert_iff_of_forall_ge {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ (x : α), x ∈ s → a ≤ x) : StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s

theorem strictAntiOn_insert_iff_of_forall_le {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ (x : α), x ∈ s → x ≤ a) : StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

theorem strictAntiOn_insert_iff_of_forall_ge {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : ∀ (x : α), x ∈ s → a ≤ x) : StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

theorem Function.monotoneOn_of_rightInvOn_of_mapsTo {α : Type u_4} {β : Type u_5} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : MonotoneOn ψ s

theorem Function.antitoneOn_of_rightInvOn_of_mapsTo {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) : AntitoneOn ψ s