theorem max_right_eq_of_max_eq_and_ne {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : max a b = c) (h₂ : a ≠ c) : b = c

@[instance_reducible, instance 100]

instance leOfOrd' {α : Type u_1} [Ord α] : LE α

Equations

• leOfOrd' = { le := fun (a b : α) => (compare a b).isLE = true }

@[instance_reducible, instance 100]

instance ltOfOrd' {α : Type u_1} [Ord α] : LT α

Equations

• ltOfOrd' = { lt := fun (a b : α) => (compare a b).isLT = true }

@[instance_reducible, instance 100]

instance minOfOrd' {α : Type u_1} [Ord α] : Min α

Equations

• minOfOrd' = { min := fun (a b : α) => if (compare a b).isLE = true then a else b }

@[instance_reducible, instance 100]

instance maxOfOrd' {α : Type u_1} [Ord α] : Max α

Equations

• maxOfOrd' = { max := fun (a b : α) => if (compare a b).isLE = true then b else a }

theorem Ord.le_def {α : Type u_1} [ha : Ord α] {a b : α} : a ≤ b ↔ (compare a b).isLE = true

theorem Ord.lt_def {α : Type u_1} [ha : Ord α] {a b : α} : a < b ↔ (compare a b).isLT = true

@[instance_reducible]

instance instDecidableRelLt_projects {α : Type u_1} [ha : Ord α] : DecidableRel LT.lt

Equations

• instDecidableRelLt_projects a b = ⋯.mpr inferInstance

theorem compare_eq {α : Type u_1} [ha : LinearOrder α] {a b : α} : compare a b = if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

@[reducible]

def Preorder.ofOrd {α : Type u_1} [ha : Ord α] (h_refl : ∀ (a : α), a ≤ a) (h_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) (h_lt : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) : Preorder α

Equations

• Preorder.ofOrd h_refl h_trans h_lt = { toLE := leOfOrd', toLT := ltOfOrd', le_refl := h_refl, le_trans := h_trans, lt_iff_le_not_ge := h_lt }

@[reducible]

def PartialOrder.ofOrd {α : Type u_1} [ha : Ord α] (h_refl : ∀ (a : α), a ≤ a) (h_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) (h_lt : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (h_ant : ∀ (a b : α), a ≤ b → b ≤ a → a = b) : PartialOrder α

Equations

• PartialOrder.ofOrd h_refl h_trans h_lt h_ant = { toPreorder := Preorder.ofOrd h_refl h_trans h_lt, le_antisymm := h_ant }

@[reducible]

def LinearOrder.ofOrd {α : Type u_1} [ha : Ord α] (h_refl : ∀ (a : α), a ≤ a) (h_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) (h_lt : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (h_ant : ∀ (a b : α), a ≤ b → b ≤ a → a = b) (h_tot : ∀ (a b : α), a ≤ b ∨ b ≤ a) : LinearOrder α

Equations

• LinearOrder.ofOrd h_refl h_trans h_lt h_ant h_tot = { toPartialOrder := PartialOrder.ofOrd h_refl h_trans h_lt h_ant, toMin := minOfOrd', toMax := maxOfOrd', toOrd := ha, le_total := h_tot, toDecidableLE := inferInstance, toDecidableEq := inferInstance, toDecidableLT := inferInstance, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

theorem isLe_compare_iff_le {α : Type u_1} [ha : LinearOrder α] {x y : α} : (compare x y).isLE = true ↔ x ≤ y

theorem isLt_compare_iff_lt {α : Type u_1} [ha : LinearOrder α] {x y : α} : (compare x y).isLT = true ↔ x < y

theorem instDistribLatticeOfLinearOrder_toSemilatticeInf_toLE_eq {α : Type u_1} [ha : LinearOrder α] : instDistribLatticeOfLinearOrder.toSemilatticeInf.toLE = ha.toLE

@[reducible]

def equivToLinearOrderAux {α : Type u_1} {β : Type u_2} [ha : LinearOrder α] (e : α ≃ β) : LinearOrder β

Equations

• equivToLinearOrderAux e = LinearOrder.ofOrd ⋯ ⋯ ⋯ ⋯ ⋯

theorem min_def₁ {α : Type u_1} [ha : LinearOrder α] : min = fun (x y : α) => if x ≤ y then x else y

theorem max_def₁ {α : Type u_1} [ha : LinearOrder α] : max = fun (x y : α) => if x ≤ y then y else x

@[reducible]

def Equiv.toLinearOrder {α : Type u_1} {β : Type u_2} [ha : LinearOrder α] (e : α ≃ β) : LinearOrder β

Equations

• e.toLinearOrder = { le := fun (x y : β) => e.invFun x ≤ e.invFun y, lt := fun (x y : β) => e.invFun x < e.invFun y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun (x y : β) => e.toFun (min (e.invFun x) (e.invFun y)), max := fun (x y : β) => e.toFun (max (e.invFun x) (e.invFun y)), compare := fun (x y : β) => compare (e.invFun x) (e.invFun y), le_total := ⋯, toDecidableLE := fun (a b : β) => LinearOrder.toDecidableLE (e.invFun a) (e.invFun b), toDecidableEq := fun (a b : β) => ⋯.mpr inferInstance, toDecidableLT := fun (a b : β) => id inferInstance, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

theorem equivToLinearOrderAux_eq : @equivToLinearOrderAux = @Equiv.toLinearOrder

theorem false_of_lt_and_lt {α : Type u_1} [ha : LinearOrder α] {a b : α} (h₁ : a < b) (h₂ : b < a) : False

@[simp]

theorem not_lt_and_lt {α : Type u_1} [ha : LinearOrder α] {a b : α} : ¬(a < b ∧ b < a)

theorem max_eq_ite {α : Type u_1} [ha : LinearOrder α] {a b : α} : max a b = if b ≤ a then a else b

theorem abs_add_le_max_add_max {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] (a b x y : α) : |a + b| ≤ max |a| x + max y |b|

theorem nonneg_of_abs_le {α : Type u_1} {a b : α} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] (h : |a| ≤ b) : 0 ≤ b

theorem pos_of_abs_lt {α : Type u_1} {a b : α} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] (h : |a| < b) : 0 < b

class InjectiveOfNat (α : Type u_1) [ha : Semiring α] : Prop

• h : Function.Injective fun (n : ℕ) => OfNat.ofNat n

instance instInjectiveOfNatNat : InjectiveOfNat ℕ

instance instInjectiveOfNatInt : InjectiveOfNat ℤ

instance instInjectiveOfNatReal : InjectiveOfNat ℝ

@[simp]

theorem add_self_eq_zero_iff {α : Type u_1} [ha₂ : Ring α] [ha₄ : NoZeroDivisors α] [ha₅ : InjectiveOfNat α] {a : α} : a + a = 0 ↔ a = 0

class LocallyFiniteOrderList (α : Type u_1) extends LinearOrder α : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : min a b = if a ≤ b then a else b
• max_def (a b : α) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• listIcc : α → α → List α
• sortedLT_listIcc {a b : α} : (listIcc a b).SortedLT
• mem_listIcc {a b x : α} : x ∈ listIcc a b ↔ a ≤ x ∧ x ≤ b

@[instance_reducible]

instance instLocallyFiniteOrderListNat : LocallyFiniteOrderList ℕ

Equations

• instLocallyFiniteOrderListNat = { toLinearOrder := Nat.instLinearOrder, listIcc := fun (a b : ℕ) => List.map (fun (x : ℕ) => a + x) (List.range (b + 1 - a)), sortedLT_listIcc := @instLocallyFiniteOrderListNat._proof_1, mem_listIcc := @instLocallyFiniteOrderListNat._proof_4 }

@[instance_reducible]

instance instLocallyFiniteOrderListInt : LocallyFiniteOrderList ℤ

Equations

• instLocallyFiniteOrderListInt = { toLinearOrder := Int.instLinearOrder, listIcc := fun (a b : ℤ) => List.map (fun (x : ℤ) => a + x) do let a ← List.range (b + 1 - a).toNat pure ↑a, sortedLT_listIcc := @instLocallyFiniteOrderListInt._proof_3, mem_listIcc := @instLocallyFiniteOrderListInt._proof_4 }

def List.icc {α : Type u_1} [ha : LocallyFiniteOrderList α] : α → α → List α

Equations

• List.icc = LocallyFiniteOrderList.listIcc

@[simp]

theorem List.sortedLT_icc {α : Type u_1} [ha : LocallyFiniteOrderList α] {a b : α} : (icc a b).SortedLT

@[simp]

theorem List.sortedLE_icc {α : Type u_1} [ha : LocallyFiniteOrderList α] {a b : α} : (icc a b).SortedLE

@[simp]

theorem List.mem_icc {α : Type u_1} [ha : LocallyFiniteOrderList α] {a b x : α} : x ∈ icc a b ↔ a ≤ x ∧ x ≤ b

@[simp]

theorem List.icc_eq_nil_iff {α : Type u_1} [ha : LocallyFiniteOrderList α] {a b : α} : icc a b = [] ↔ b < a

@[simp]

theorem List.nodup_icc {α : Type u_1} [ha : LocallyFiniteOrderList α] {x y : α} : (icc x y).Nodup

@[simp]

theorem List.length_icc_int_nat {z : ℤ} {a b : ℕ} : (icc (z - ↑a) (z + ↑b)).length = a + b + 1

theorem List.icc_eq_range {n m : ℕ} (h : n ≤ m) : icc n m = map (fun (x : ℕ) => n + x) (range (m - n + 1))

theorem List.icc_split (k : ℕ) {n m : ℕ} (h₁ : n ≤ k) (h₂ : k < m) : icc n m = icc n k ++ icc (k + 1) m

@[simp]

theorem min_sub_one_lt_left {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : min a b - 1 < a

@[simp]

theorem min_sub_one_lt_right {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : min a b - 1 < b

@[simp]

theorem left_lt_max_add_one {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : a < max a b + 1

@[simp]

theorem right_lt_max_add_one {α : Type u_1} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : IsOrderedAddMonoid α] [ha₄ : ZeroLEOneClass α] [ha₅ : NeZero 1] {a b : α} : b < max a b + 1

theorem min_eq_ite {α : Type u_2} [ha : LinearOrder α] {x y : α} : min x y = if x ≤ y then x else y

theorem abs_eq_ite {α : Type u_2} [ha₁ : LinearOrder α] [hs₂ : AddGroup α] [ha₃ : AddLeftMono α] {x : α} : |x| = if 0 ≤ x then x else -x

theorem bddBelow_range_of_forall_le {ι : Type u_2} {α : Type u_3} [ha : LinearOrder α] {f : ι → α} (x : α) (h : ∀ (i : ι), x ≤ f i) : BddBelow (Set.range f)

theorem bddAbove_range_of_forall_le {ι : Type u_2} {α : Type u_3} [ha : LinearOrder α] {f : ι → α} (x : α) (h : ∀ (i : ι), f i ≤ x) : BddAbove (Set.range f)

theorem bddBelow_range {ι : Type u_2} {α : Type u_3} [ha : LinearOrder α] {f : ι → α} : BddBelow (Set.range f) ↔ ∃ (x : α), ∀ (i : ι), x ≤ f i

theorem bddAbove_range {ι : Type u_2} {α : Type u_3} [ha : LinearOrder α] {f : ι → α} : BddAbove (Set.range f) ↔ ∃ (x : α), ∀ (i : ι), f i ≤ x

theorem bddBelow_range_neg {ι : Type u_2} {α : Type u_3} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] [ha₄ : AddRightMono α] {f : ι → α} : BddBelow (Set.range (-f)) ↔ BddAbove (Set.range f)

theorem bddAbove_range_neg {ι : Type u_2} {α : Type u_3} [ha₁ : LinearOrder α] [ha₂ : Ring α] [ha₃ : AddLeftMono α] [ha₄ : AddRightMono α] {f : ι → α} : BddAbove (Set.range (-f)) ↔ BddBelow (Set.range f)

noncomputable def fintypeIdx {α : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Fintype α] (x : α) : ℕ

Equations

• fintypeIdx x = List.idxOf x Finset.univ.toList

@[simp]

theorem fintypeIdx_eq_iff {α : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Fintype α] {x y : α} : fintypeIdx x = fintypeIdx y ↔ x = y

@[reducible]

noncomputable def fintypeToLinearOrder {α : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Fintype α] : LinearOrder α

Equations

• fintypeToLinearOrder = { le := fun (a b : α) => fintypeIdx a ≤ fintypeIdx b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun (a b : α) => if (fun (a b : α) => fintypeIdx a ≤ fintypeIdx b) a b then a else b, max := fun (a b : α) => if (fun (a b : α) => fintypeIdx a ≤ fintypeIdx b) a b then b else a, compare := fun (a b : α) => compareOfLessAndEq a b, le_total := ⋯, toDecidableLE := inferInstance, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

theorem abs_sub_lt_iff' {x y z : ℝ} : |x - y| < z ↔ y - z < x ∧ x < y + z

theorem abs_sub_lt_trans {α : Type u_2} [LinearOrder α] [NormedField α] [IsStrictOrderedRing α] {a c e : α} (b : α) (h : |a - b| + |b - c| < e) : |a - c| < e

theorem abs_sub_le_trans {α : Type u_2} [LinearOrder α] [NormedField α] [IsStrictOrderedRing α] {a c e : α} (b : α) (h : |a - b| + |b - c| ≤ e) : |a - c| ≤ e

theorem abs_sub_lt_trans_half {α : Type u_2} [LinearOrder α] [NormedField α] [IsStrictOrderedRing α] {a c e : α} (b : α) (h₁ : |a - b| < e / 2) (h₂ : |b - c| < e / 2) : |a - c| < e

theorem abs_sub_le_trans_half {α : Type u_2} [LinearOrder α] [NormedField α] [IsStrictOrderedRing α] {a c e : α} (b : α) (h₁ : |a - b| ≤ e / 2) (h₂ : |b - c| ≤ e / 2) : |a - c| ≤ e

structure LeCnd {α : Type u_2} (le : α → α → Prop) : Prop

• refl (x : α) : le x x
• trans (x y z : α) : le x y → le y z → le x z
• antisymm (x y : α) : le x y → le y x → x = y
• total (x y : α) : le x y ∨ le y x

theorem exi_leCnd {α : Type u_2} : ∃ (le : α → α → Prop), LeCnd le

def leClassical {α : Type u_2} : α → α → Prop

Equations

• leClassical = Classical.epsilon fun (x : α → α → Prop) => LeCnd x

theorem leCnd_leClassical {α : Type u_2} : LeCnd leClassical

@[reducible]

noncomputable def linearOrderClassical {α : Type u_2} : LinearOrder α

Equations

• linearOrderClassical = { le := leClassical, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun (a b : α) => if leClassical a b then a else b, max := fun (a b : α) => if leClassical a b then b else a, compare := fun (a b : α) => compareOfLessAndEq a b, le_total := ⋯, toDecidableLE := inferInstance, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

@[instance_reducible, instance 100]

noncomputable instance instLinearOrderOfDecidable_projects {α : Type u_2} [(P : Prop) → Decidable P] : LinearOrder α

Equations

• instLinearOrderOfDecidable_projects = linearOrderClassical

theorem le_congr {α : Type u_2} [ha : LinearOrder α] {a b c d : α} (h₁ : a = c) (h₂ : b = d) : a ≤ b ↔ c ≤ d

theorem exists_not_le_of_sInf_not_mem {α : Type u_2} [ha : CompleteLattice α] {s : Set α} {x : α} (h : sInf s ∉ s) (hx : x ∈ s) : ∃ y ∈ s, ¬x ≤ y

theorem exists_not_le_of_sSup_not_mem {α : Type u_2} [ha : CompleteLattice α] {s : Set α} {x : α} (h : sSup s ∉ s) (hx : x ∈ s) : ∃ y ∈ s, ¬y ≤ x

@[simp]

theorem sInf_mem_iff {α : Type u_2} [ha : CompleteLattice α] {s : Set α} : sInf s ∈ s ↔ ∃ x ∈ s, ∀ y ∈ s, x ≤ y

@[simp]

theorem sSup_mem_iff {α : Type u_2} [ha : CompleteLattice α] {s : Set α} : sSup s ∈ s ↔ ∃ x ∈ s, ∀ y ∈ s, y ≤ x

theorem List.eq_of_sortedLE_and_perm {α : Type u_2} {xs ys : List α} [ha : LinearOrder α] (h₁ : xs.SortedLE) (h₂ : ys.SortedLE) (h₃ : xs.Perm ys) : xs = ys