Documentation

Mathlib.Data.Set.Monotone

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.domRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (h : Monotone f) (s : Set α) :

Monotone (s.domRestrict f)

@[deprecated Monotone.domRestrict (since := "2026-07-19")]

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

Monotone (s.domRestrict f)

Alias of Monotone.domRestrict.

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_domRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMono (s.domRestrict f) ↔ StrictMonoOn f s

theorem StrictMonoOn.domRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMonoOn f s → StrictMono (s.domRestrict f)

Alias of the reverse direction of strictMono_domRestrict.

theorem StrictMono.of_domRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMono (s.domRestrict f) → StrictMonoOn f s

Alias of the forward direction of strictMono_domRestrict.

@[deprecated strictMono_domRestrict (since := "2026-07-19")]

theorem strictMono_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} :

StrictMono (s.domRestrict f) ↔ StrictMonoOn f s

Alias of strictMono_domRestrict.

@[deprecated StrictMono.of_domRestrict (since := "2026-07-19")]

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

StrictMono (s.domRestrict f) → StrictMonoOn f s

Alias of StrictMono.of_domRestrict.

Alias of the forward direction of strictMono_domRestrict.

@[deprecated StrictMonoOn.domRestrict (since := "2026-07-19")]

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

StrictMonoOn f s → StrictMono (s.domRestrict f)

Alias of StrictMonoOn.domRestrict.

Alias of the reverse direction of strictMono_domRestrict.

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_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :

MonotoneOn ψ s

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

StrictMonoOn ψ 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

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

StrictAntiOn ψ s

theorem Function.monotone_of_rightInverse {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} (hφ : Monotone φ) (φψ : RightInverse ψ φ) :

theorem Function.strictMono_of_rightInverse {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {φ : β → α} {ψ : α → β} (hφ : StrictMono φ) (φψ : RightInverse ψ φ) :

theorem Function.antitone_of_rightInverse {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : β → α} {ψ : α → β} (hφ : Antitone φ) (φψ : RightInverse ψ φ) :

theorem Function.strictAnti_of_rightInverse {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {φ : β → α} {ψ : α → β} (hφ : StrictAnti φ) (φψ : RightInverse ψ φ) :