Monotone functions on bounded orders

Top, bottom element

theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤

theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) : f a = f ⊤ ↔ a = ⊤

theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β} (H : StrictMono f) {a : α} (h_top : f a = ⊤) (x : α) : x ≤ a

theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥

theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) : f a = f ⊥ ↔ a = ⊥

theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] [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

theorem monotone_and {α : Type u} [Preorder α] {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun (x : α) => p x ∧ q x

theorem monotone_or {α : Type u} [Preorder α] {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun (x : α) => p x ∨ q x

theorem monotone_le {α : Type u} [Preorder α] {x : α} : Monotone fun (x_1 : α) => x ≤ x_1

theorem monotone_lt {α : Type u} [Preorder α] {x : α} : Monotone fun (x_1 : α) => x < x_1

theorem antitone_le {α : Type u} [Preorder α] {x : α} : Antitone fun (x_1 : α) => x_1 ≤ x

theorem antitone_lt {α : Type u} [Preorder α] {x : α} : Antitone fun (x_1 : α) => x_1 < x

theorem Monotone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) : Monotone fun (y : α) => ∀ (x : β), P x y

theorem Antitone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) : Antitone fun (y : α) => ∀ (x : β), P x y

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

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

theorem Monotone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) : Monotone fun (y : α) => ∃ (x : β), P x y

theorem Antitone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) : Antitone fun (y : α) => ∃ (x : β), P x y

theorem forall_ge_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∀ (x : α), x ≥ x₀ → P x) ↔ P x₀

theorem forall_le_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Antitone P) : (∀ (x : α), x ≤ x₀ → P x) ↔ P x₀