max and min

This file proves basic properties about maxima and minima on a LinearOrder.

Tags

min, max

theorem le_min_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : c ≤ a ⊓ b ↔ c ≤ a ∧ c ≤ b

theorem le_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

theorem min_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊓ b ≤ c ↔ a ≤ c ∨ b ≤ c

theorem max_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem lt_min_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a < b ⊓ c ↔ a < b ∧ a < c

theorem lt_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a < b ⊔ c ↔ a < b ∨ a < c

theorem min_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊓ b < c ↔ a < c ∨ b < c

theorem max_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊔ b < c ↔ a < c ∧ b < c

theorem max_le_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} : a ≤ c → b ≤ d → a ⊔ b ≤ c ⊔ d

theorem max_le_max_left {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) : c ⊔ a ≤ c ⊔ b

theorem max_le_max_right {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) : a ⊔ c ≤ b ⊔ c

theorem min_le_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} : a ≤ c → b ≤ d → a ⊓ b ≤ c ⊓ d

theorem min_le_min_left {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) : c ⊓ a ≤ c ⊓ b

theorem min_le_min_right {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) : a ⊓ c ≤ b ⊓ c

theorem le_max_of_le_left {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ b → a ≤ b ⊔ c

theorem le_max_of_le_right {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ c → a ≤ b ⊔ c

theorem lt_max_of_lt_left {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < b) : a < b ⊔ c

theorem lt_max_of_lt_right {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < c) : a < b ⊔ c

theorem min_le_of_left_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ c → a ⊓ b ≤ c

theorem min_le_of_right_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : b ≤ c → a ⊓ b ≤ c

theorem min_lt_of_left_lt {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < c) : a ⊓ b < c

theorem min_lt_of_right_lt {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : b < c) : a ⊓ b < c

theorem max_min_distrib_left {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

theorem max_min_distrib_right {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

theorem min_max_distrib_left {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

theorem min_max_distrib_right {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

theorem min_le_max {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊓ b ≤ a ⊔ b

theorem min_eq_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊓ b = a ↔ a ≤ b

theorem min_eq_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊓ b = b ↔ b ≤ a

theorem max_eq_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊔ b = a ↔ b ≤ a

theorem max_eq_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊔ b = b ↔ a ≤ b

theorem min_cases {α : Type u} [LinearOrder α] (a : α) (b : α) : a ⊓ b = a ∧ a ≤ b ∨ a ⊓ b = b ∧ b < a

For elements a and b of a linear order, either min a b = a and a ≤ b, or min a b = b and b < a. Use cases on this lemma to automate linarith in inequalities

theorem max_cases {α : Type u} [LinearOrder α] (a : α) (b : α) : a ⊔ b = a ∧ b ≤ a ∨ a ⊔ b = b ∧ a < b

For elements a and b of a linear order, either max a b = a and b ≤ a, or max a b = b and a < b. Use cases on this lemma to automate linarith in inequalities

theorem min_eq_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊓ b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a

theorem max_eq_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊔ b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b

theorem min_lt_min_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊓ c < b ⊓ c ↔ a < b ∧ a < c

theorem min_lt_min_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊓ b < a ⊓ c ↔ b < c ∧ b < a

theorem max_lt_max_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊔ c < b ⊔ c ↔ a < b ∧ c < b

theorem max_lt_max_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ⊔ b < a ⊔ c ↔ b < c ∧ a < c

instance max_idem {α : Type u} [LinearOrder α] : Std.IdempotentOp max

An instance asserting that max a a = a

Equations

• ⋯ = ⋯

instance min_idem {α : Type u} [LinearOrder α] : Std.IdempotentOp min

An instance asserting that min a a = a

Equations

• ⋯ = ⋯

theorem min_lt_max {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊓ b < a ⊔ b ↔ a ≠ b

theorem max_lt_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) : a ⊔ b < c ⊔ d

theorem min_lt_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) : a ⊓ b < c ⊓ d

theorem min_right_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b

theorem Max.left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

theorem Max.right_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b

theorem MonotoneOn.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (a ⊔ b) = f a ⊔ f b

theorem MonotoneOn.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (a ⊓ b) = f a ⊓ f b

theorem AntitoneOn.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (a ⊔ b) = f a ⊓ f b

theorem AntitoneOn.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (a ⊓ b) = f a ⊔ f b

theorem Monotone.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {a : α} {b : α} (hf : Monotone f) : f (a ⊔ b) = f a ⊔ f b

theorem Monotone.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {a : α} {b : α} (hf : Monotone f) : f (a ⊓ b) = f a ⊓ f b

theorem Antitone.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {a : α} {b : α} (hf : Antitone f) : f (a ⊔ b) = f a ⊓ f b

theorem Antitone.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {a : α} {b : α} (hf : Antitone f) : f (a ⊓ b) = f a ⊔ f b

theorem min_choice {α : Type u} [LinearOrder α] (a : α) (b : α) : a ⊓ b = a ∨ a ⊓ b = b

theorem max_choice {α : Type u} [LinearOrder α] (a : α) (b : α) : a ⊔ b = a ∨ a ⊔ b = b

theorem le_of_max_le_left {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a ⊔ b ≤ c) : a ≤ c

theorem le_of_max_le_right {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a ⊔ b ≤ c) : b ≤ c

instance instCommutativeMax {α : Type u} [LinearOrder α] : Std.Commutative max

Equations

• ⋯ = ⋯

instance instAssociativeMax {α : Type u} [LinearOrder α] : Std.Associative max

Equations

• ⋯ = ⋯

instance instCommutativeMin {α : Type u} [LinearOrder α] : Std.Commutative min

Equations

• ⋯ = ⋯

instance instAssociativeMin {α : Type u} [LinearOrder α] : Std.Associative min

Equations

• ⋯ = ⋯

theorem max_left_commutative {α : Type u} [LinearOrder α] : LeftCommutative max

theorem min_left_commutative {α : Type u} [LinearOrder α] : LeftCommutative min