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 : Set.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 : Set.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 : Set.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 : Set.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)
:
theorem
AntitoneOn.monotone
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{f : α → β}
[Preorder α]
[Preorder β]
(h : AntitoneOn f s)
:
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)
Monotone #
theorem
StrictMonoOn.injOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
{f : α → β}
{s : Set α}
(H : StrictMonoOn f s)
:
Set.InjOn f s
theorem
StrictAntiOn.injOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[Preorder β]
{f : α → β}
{s : Set α}
(H : StrictAntiOn f s)
:
Set.InjOn f s
theorem
StrictMonoOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictMonoOn g t)
(hf : StrictMonoOn f s)
(hs : Set.MapsTo f s t)
:
StrictMonoOn (g ∘ f) s
theorem
StrictMonoOn.comp_strictAntiOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictMonoOn g t)
(hf : StrictAntiOn f s)
(hs : Set.MapsTo f s t)
:
StrictAntiOn (g ∘ f) s
theorem
StrictAntiOn.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictAntiOn g t)
(hf : StrictAntiOn f s)
(hs : Set.MapsTo f s t)
:
StrictMonoOn (g ∘ f) s
theorem
StrictAntiOn.comp_strictMonoOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
[Preorder γ]
{g : β → γ}
{f : α → β}
{s : Set α}
{t : Set β}
(hg : StrictAntiOn g t)
(hf : StrictMonoOn f s)
(hs : Set.MapsTo f s t)
:
StrictAntiOn (g ∘ f) s
@[simp]
theorem
strictMono_restrict
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Preorder β]
{f : α → β}
{s : Set α}
:
StrictMono (s.restrict f) ↔ StrictMonoOn f s
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.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
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
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