# Monotone functions on bounded orders #

### Top, bottom element #

source
theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) :
f a = f ⊤ ↔ a = ⊤
source
theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) :
f a = f ⊤ ↔ a = ⊤
source
theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β} (H : StrictMono f) {a : α} (h_top : f a = ⊤) (x : α) :
x ≤ a
source
theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) :
f a = f ⊥ ↔ a = ⊥
source
theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) :
f a = f ⊥ ↔ a = ⊥
source
theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] [OrderBot β] {f : α → β} (H : StrictMono f) {a : α} (h_bot : f a = ⊥) (x : α) :
a ≤ x

#### In this section we prove some properties about monotone and antitone operations on `Prop` #

source
theorem monotone_and {α : Type u} [Preorder α] {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
Monotone fun (x : α) => p x ∧ q x
source
theorem monotone_or {α : Type u} [Preorder α] {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :
Monotone fun (x : α) => p x ∨ q x
source
theorem monotone_le {α : Type u} [Preorder α] {x : α} :
Monotone fun (x_1 : α) => x ≤ x_1
source
theorem monotone_lt {α : Type u} [Preorder α] {x : α} :
Monotone fun (x_1 : α) => x < x_1
source
theorem antitone_le {α : Type u} [Preorder α] {x : α} :
Antitone fun (x_1 : α) => x_1 ≤ x
source
theorem antitone_lt {α : Type u} [Preorder α] {x : α} :
Antitone fun (x_1 : α) => x_1 < x
source
theorem Monotone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :
Monotone fun (y : α) => ∀ (x : β), P x y
source
theorem Antitone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :
Antitone fun (y : α) => ∀ (x : β), P x y
source
theorem Monotone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Monotone (P x)) :
Monotone fun (y : α) => ∀ (x : β), x ∈ s → P x y
source
theorem Antitone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Antitone (P x)) :
Antitone fun (y : α) => ∀ (x : β), x ∈ s → P x y
source
theorem Monotone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :
Monotone fun (y : α) => ∃ (x : β), P x y
source
theorem Antitone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :
Antitone fun (y : α) => ∃ (x : β), P x y
source
theorem forall_ge_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Monotone P) :
(∀ (x : α), x ≥ x₀ → P x) ↔ P x₀
source
theorem forall_le_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Antitone P) :
(∀ (x : α), x ≤ x₀ → P x) ↔ P x₀