Loogle!

Result

Found 586 declarations mentioning Order.succ. Of these, 453 have a name containing "succ". Of these, only the first 200 are shown.

Order.succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] : α → α
Order.succ_mono 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] : Monotone Order.succ
Order.wcovBy_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] (a : α) : a ⩿ Order.succ a
Order.succ.eq_1 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] : Order.succ = SuccOrder.succ
Order.le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] (a : α) : a ≤ Order.succ a
Order.succ_strictMono 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] : StrictMono Order.succ
Order.gc_pred_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] : GaloisConnection Order.pred Order.succ
Order.le_succ_iterate 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] (k : ℕ) (x : α) : x ≤ Order.succ^[k] x
Order.covBy_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : a ⋖ Order.succ a
Order.lt_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : a < Order.succ a
IsMax.of_succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : Order.succ a ≤ a → IsMax a
IsMax.succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : IsMax a → Order.succ a ≤ a
Order.le_succ_of_wcovBy 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a ⩿ b) : b ≤ Order.succ a
Order.max_of_succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : Order.succ a ≤ a → IsMax a
WCovBy.le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a ⩿ b) : b ≤ Order.succ a
Order.covBy_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (h : ¬IsMax a) : a ⋖ Order.succ a
Order.le_succ_pred 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] (a : α) : a ≤ Order.succ (Order.pred a)
Order.lt_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : ¬IsMax a → a < Order.succ a
Order.pred_succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [PredOrder α] [SuccOrder α] (a : α) : Order.pred (Order.succ a) ≤ a
Order.succ_le_iff_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : Order.succ a ≤ a ↔ IsMax a
Order.lt_succ_iff_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} : a < Order.succ a ↔ ¬IsMax a
Order.succ_le_of_lt 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} : a < b → Order.succ a ≤ b
LT.lt.succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} : a < b → Order.succ a ≤ b
IsMax.succ_eq 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} : IsMax a → Order.succ a = a
Order.Ici_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Ici (Order.succ a) = Set.Ioi a
Order.succ_eq_iff_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} : Order.succ a = a ↔ IsMax a
WithTop.instSuccOrder 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] : SuccOrder (WithTop α)
CovBy.succ_eq 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} (h : a ⋖ b) : Order.succ a = b
Order.Ici_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Ici (Order.succ a) = Set.Ioi a
Order.Iic_subset_Iio_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Iic a ⊆ Set.Iio (Order.succ a)
Order.succ_eq_of_covBy 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} (h : a ⋖ b) : Order.succ a = b
Order.Icc_succ_left 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Icc (Order.succ a) b = Set.Ioc a b
Order.Ico_succ_left 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ico (Order.succ a) b = Set.Ioo a b
Order.succ_le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a ≤ b) : Order.succ a ≤ Order.succ b
Order.Iic_subset_Iio_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Iic a ⊆ Set.Iio (Order.succ a)
Order.lt_succ_of_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : a ≤ b → a < Order.succ b
Order.Icc_subset_Ico_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Icc a b ⊆ Set.Ico a (Order.succ b)
Order.Icc_succ_left_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) : Set.Icc (Order.succ a) b = Set.Ioc a b
Order.Ico_succ_left_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) : Set.Ico (Order.succ a) b = Set.Ioo a b
Order.Ioc_subset_Ioo_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ioc a b ⊆ Set.Ioo a (Order.succ b)
Order.succ_le_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a ≤ b ↔ a < b
Order.lt_succ_of_le_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hab : b ≤ a) (ha : ¬IsMax a) : b < Order.succ a
Order.Icc_subset_Ico_succ_right_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Icc a b ⊆ Set.Ico a (Order.succ b)
Order.Ioc_subset_Ioo_succ_right_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Ioc a b ⊆ Set.Ioo a (Order.succ b)
Order.le_succ_iff_pred_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [PredOrder α] [SuccOrder α] {a b : α} : b ≤ Order.succ a ↔ Order.pred b ≤ a
Order.pred_le_iff_le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] {a b : α} : Order.pred a ≤ b ↔ a ≤ Order.succ b
Order.succ_le_iff_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) : Order.succ a ≤ b ↔ a < b
Order.succ_lt_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (hab : a < b) : Order.succ a < Order.succ b
WithBot.orderSucc_coe 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : α) : Order.succ ↑a = ↑(Order.succ a)
Order.pred_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] [NoMaxOrder α] (a : α) : Order.pred (Order.succ a) = a
Order.succ_eq_iff_covBy 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a = b ↔ a ⋖ b
Order.succ_lt_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a b : α} (h : a < b) (hb : ¬IsMax b) : Order.succ a < Order.succ b
Order.succ_ne_bot 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderBot α] [Nontrivial α] (a : α) : Order.succ a ≠ ⊥
Order.succ_pred 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] [NoMinOrder α] (a : α) : Order.succ (Order.pred a) = a
Order.pred_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α} (h : ¬IsMax a) : Order.pred (Order.succ a) = a
Order.succ_pred_of_not_isMin 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] {a : α} (h : ¬IsMin a) : Order.succ (Order.pred a) = a
Order.le_iff_eq_or_succ_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} : a ≤ b ↔ a = b ∨ Order.succ a ≤ b
Order.le_iff_eq_or_succ_le' 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} : a ≤ b ↔ b = a ∨ Order.succ a ≤ b
WithBot.orderSucc_bot 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] : Order.succ ⊥ = ↑⊥
Order.bot_lt_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderBot α] [Nontrivial α] (a : α) : ⊥ < Order.succ a
Order.succ_eq_sInf 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [CompleteLattice α] [SuccOrder α] (a : α) : Order.succ a = sInf (Set.Ioi a)
Order.succ_top 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [OrderTop α] : Order.succ ⊤ = ⊤
Order.isMax_iterate_succ_of_eq_of_ne 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {n m : ℕ} (h_eq : Order.succ^[n] a = Order.succ^[m] a) (h_ne : n ≠ m) : IsMax (Order.succ^[n] a)
Order.isMax_iterate_succ_of_eq_of_lt 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [SuccOrder α] {a : α} {n m : ℕ} (h_eq : Order.succ^[n] a = Order.succ^[m] a) (h_lt : n < m) : IsMax (Order.succ^[n] a)
Order.lt_succ_iff_ne_top 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [OrderTop α] : a < Order.succ a ↔ a ≠ ⊤
Order.succ_le_iff_eq_top 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [OrderTop α] : Order.succ a ≤ a ↔ a = ⊤
Order.succ_injective 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] : Function.Injective Order.succ
Order.not_isMin_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [Nontrivial α] (a : α) : ¬IsMin (Order.succ a)
Order.le_and_le_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} : a ≤ b ∧ b ≤ Order.succ a ↔ b = a ∨ b = Order.succ a
Order.le_le_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} : a ≤ b ∧ b ≤ Order.succ a ↔ b = a ∨ b = Order.succ a
Order.le_succ_and_le_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] {a b : α} : b ≤ Order.succ a ∧ a ≤ b ↔ b = a ∨ b = Order.succ a
WithBot.succ_unbot 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : WithBot α) (ha : a ≠ ⊥) : Order.succ (a.unbot ha) = (Order.succ a).unbot ⋯
WithTop.succ_coe_of_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] {a : α} (h : IsMax a) : Order.succ ↑a = ⊤
WithTop.succ_coe 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] [NoMaxOrder α] {a : α} : Order.succ ↑a = ↑(Order.succ a)
WithTop.succ_coe_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [(a : α) → Decidable (Order.succ a = a)] {a : α} (h : ¬IsMax a) : Order.succ ↑a = ↑(Order.succ a)
Order.succ_eq_csInf 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) : Order.succ a = sInf (Set.Ioi a)
isMax_of_succ_notMem 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : ↑s} (h : Order.succ ↑a ∉ s) : IsMax a
Order.le_of_lt_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} : a < Order.succ b → a ≤ b
Order.pred_succ_iterate_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] (i : α) (n : ℕ) (hin : ¬IsMax (Order.succ^[n - 1] i)) : Order.pred^[n] (Order.succ^[n] i) = i
Order.succ_pred_iterate_of_not_isMin 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [PartialOrder α] [SuccOrder α] [PredOrder α] (i : α) (n : ℕ) (hin : ¬IsMin (Order.pred^[n - 1] i)) : Order.succ^[n] (Order.pred^[n] i) = i
Order.succ_eq_iInf 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [CompleteLattice α] [SuccOrder α] (a : α) : Order.succ a = ⨅ b, ⨅ (_ : b > a), b
Order.succ_ne_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : a ≠ b → Order.succ a ≠ Order.succ b
Order.succ_eq_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a = Order.succ b ↔ a = b
Order.succ_ne_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a ≠ Order.succ b ↔ a ≠ b
succ_notMem_iff_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] [NoMaxOrder α] {a : ↑s} : Order.succ ↑a ∉ s ↔ IsMax a
Order.Iio_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Iio (Order.succ a) = Set.Iic a
Order.Iio_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Iio (Order.succ a) = Set.Iic a
Order.Ico_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ico a (Order.succ b) = Set.Icc a b
Order.Ioo_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ioo a (Order.succ b) = Set.Ioc a b
Order.Ico_succ_right_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Ico a (Order.succ b) = Set.Icc a b
Order.Ioo_succ_right_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : Set.Ioo a (Order.succ b) = Set.Ioc a b
Order.lt_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : a < Order.succ b ↔ a ≤ b
Order.Iic_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] (a : α) : Set.Iic (Order.succ a) = insert (Order.succ a) (Set.Iic a)
Order.Iio_succ_eq_insert 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Iio (Order.succ a) = insert a (Set.Iio a)
Order.lt_succ_iff_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) : b < Order.succ a ↔ b ≤ a
Order.Iio_succ_eq_insert_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (h : ¬IsMax a) : Set.Iio (Order.succ a) = insert a (Set.Iio a)
Order.le_succ_iff_eq_or_le 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} : a ≤ Order.succ b ↔ a = Order.succ b ∨ a ≤ b
Order.lt_succ_iff_eq_or_gt 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : a < Order.succ b ↔ b = a ∨ a < b
Order.lt_succ_iff_eq_or_lt 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : a < Order.succ b ↔ a = b ∨ a < b
Order.Ioo_eq_empty_iff_le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Set.Ioo a b = ∅ ↔ b ≤ Order.succ a
Order.lt_succ_iff_eq_or_lt_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (hb : ¬IsMax b) : a < Order.succ b ↔ a = b ∨ a < b
Order.succ_eq_succ_iff_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) : Order.succ a = Order.succ b ↔ a = b
Order.le_of_succ_le_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a ≤ Order.succ b → a ≤ b
Order.lt_of_succ_lt_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a < Order.succ b → a < b
Order.succ_le_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a ≤ Order.succ b ↔ a ≤ b
Order.succ_lt_succ_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] : Order.succ a < Order.succ b ↔ a < b
coe_succ_of_mem 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_3} [PartialOrder α] {s : Set α} [s.OrdConnected] [SuccOrder α] {a : ↑s} (h : Order.succ ↑a ∈ s) : ↑(Order.succ a) = Order.succ ↑a
Order.Ico_succ_right_eq_insert 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) : Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
Order.Ioo_succ_right_eq_insert 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a < b) : Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
Order.Ico_succ_right_eq_insert_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h₁ : a ≤ b) (h₂ : ¬IsMax b) : Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
Order.Ioo_succ_right_eq_insert_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h₁ : a < b) (h₂ : ¬IsMax b) : Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
OrderIso.map_succ 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} {β : Type u_2} [PartialOrder α] [SuccOrder α] [PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) : f (Order.succ a) = Order.succ (f a)
Order.succ_le_succ_iff_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) : Order.succ a ≤ Order.succ b ↔ a ≤ b
Order.succ_lt_succ_iff_of_not_isMax 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (ha : ¬IsMax a) (hb : ¬IsMax b) : Order.succ a < Order.succ b ↔ a < b
Order.Icc_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a ≤ Order.succ b) : Set.Icc a (Order.succ b) = insert (Order.succ b) (Set.Icc a b)
Order.Ioc_succ_right 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a < Order.succ b) : Set.Ioc a (Order.succ b) = insert (Order.succ b) (Set.Ioc a b)
Order.lt_succ_bot_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] [NoMaxOrder α] : a < Order.succ ⊥ ↔ a = ⊥
Order.le_succ_bot_iff 📋 Mathlib.Order.SuccPred.Basic
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} [OrderBot α] : a ≤ Order.succ ⊥ ↔ a = ⊥ ∨ a = Order.succ ⊥
Set.Ico_succ_left_eq_Ioo 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] (a b : α) : Set.Ico (Order.succ a) b = Set.Ioo a b
Set.Ici_succ_eq_Ioi 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a : α) : Set.Ici (Order.succ a) = Set.Ioi a
Set.Iio_succ_eq_Iic 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (b : α) : Set.Iio (Order.succ b) = Set.Iic b
Set.Ici_succ_eq_Ioi_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Set.Ici (Order.succ a) = Set.Ioi a
Set.Iio_succ_eq_Iic_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) : Set.Iio (Order.succ b) = Set.Iic b
Set.Icc_succ_left_eq_Ioc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Icc (Order.succ a) b = Set.Ioc a b
Set.Ico_succ_right_eq_Icc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ico a (Order.succ b) = Set.Icc a b
Set.Ioo_succ_right_eq_Ioc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ioo a (Order.succ b) = Set.Ioc a b
Set.Icc_succ_left_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) (b : α) : Set.Icc (Order.succ a) b = Set.Ioc a b
Set.Ico_succ_right_eq_Icc_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Set.Ico a (Order.succ b) = Set.Icc a b
Set.Ioo_succ_right_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Set.Ioo a (Order.succ b) = Set.Ioc a b
Set.insert_Icc_succ_left_eq_Icc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) : insert a (Set.Icc (Order.succ a) b) = Set.Icc a b
Set.insert_Ico_succ_left_eq_Ico 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a < b) : insert a (Set.Ico (Order.succ a) b) = Set.Ico a b
Set.Icc_succ_pred_eq_Ioo 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [PredOrder α] [Nontrivial α] (a b : α) : Set.Icc (Order.succ a) (Order.pred b) = Set.Ioo a b
Set.Ico_succ_succ_eq_Ioc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Set.Ico (Order.succ a) (Order.succ b) = Set.Ioc a b
Set.Ico_succ_succ_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Set.Ico (Order.succ a) (Order.succ b) = Set.Ioc a b
Set.insert_Ioc_succ_left_eq_Ioc 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a < b) : insert (Order.succ a) (Set.Ioc (Order.succ a) b) = Set.Ioc a b
Set.insert_Ico_right_eq_Ico_succ 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) : insert b (Set.Ico a b) = Set.Ico a (Order.succ b)
Set.insert_Ico_right_eq_Ico_succ_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) : insert b (Set.Ico a b) = Set.Ico a (Order.succ b)
Set.insert_Icc_right_eq_Icc_succ 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a ≤ Order.succ b) : insert (Order.succ b) (Set.Icc a b) = Set.Icc a (Order.succ b)
Set.insert_Ioc_right_eq_Ioc_succ 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) : insert (Order.succ b) (Set.Ioc a b) = Set.Ioc a (Order.succ b)
Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax 📋 Mathlib.Order.Interval.Set.SuccPred
{α : Type u_1} [LinearOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) : insert (Order.succ b) (Set.Ioc a b) = Set.Ioc a (Order.succ b)
Finset.Ico_succ_left_eq_Ioo 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] (a b : α) : Finset.Ico (Order.succ a) b = Finset.Ioo a b
Finset.Ici_succ_eq_Ioi 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [SuccOrder α] [NoMaxOrder α] (a : α) : Finset.Ici (Order.succ a) = Finset.Ioi a
Finset.Iio_succ_eq_Iic 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [SuccOrder α] [NoMaxOrder α] (b : α) : Finset.Iio (Order.succ b) = Finset.Iic b
Finset.Ici_succ_eq_Ioi_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrderTop α] [SuccOrder α] {a : α} (ha : ¬IsMax a) : Finset.Ici (Order.succ a) = Finset.Ioi a
Finset.Iio_succ_eq_Iic_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrderBot α] [SuccOrder α] {b : α} (hb : ¬IsMax b) : Finset.Iio (Order.succ b) = Finset.Iic b
Finset.Icc_succ_left_eq_Ioc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Finset.Icc (Order.succ a) b = Finset.Ioc a b
Finset.Ico_succ_right_eq_Icc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Finset.Ico a (Order.succ b) = Finset.Icc a b
Finset.Ioo_succ_right_eq_Ioc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Finset.Ioo a (Order.succ b) = Finset.Ioc a b
Finset.Icc_succ_left_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a : α} (ha : ¬IsMax a) (b : α) : Finset.Icc (Order.succ a) b = Finset.Ioc a b
Finset.Ico_succ_right_eq_Icc_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Finset.Ico a (Order.succ b) = Finset.Icc a b
Finset.Ioo_succ_right_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Finset.Ioo a (Order.succ b) = Finset.Ioc a b
Finset.Icc_succ_pred_eq_Ioo 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [PredOrder α] [Nontrivial α] (a b : α) : Finset.Icc (Order.succ a) (Order.pred b) = Finset.Ioo a b
Finset.Ico_succ_succ_eq_Ioc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] [NoMaxOrder α] (a b : α) : Finset.Ico (Order.succ a) (Order.succ b) = Finset.Ioc a b
Finset.Ico_succ_succ_eq_Ioc_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {b : α} (hb : ¬IsMax b) (a : α) : Finset.Ico (Order.succ a) (Order.succ b) = Finset.Ioc a b
Finset.insert_Icc_succ_left_eq_Icc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) : insert a (Finset.Icc (Order.succ a) b) = Finset.Icc a b
Finset.insert_Ico_succ_left_eq_Ico 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a < b) : insert a (Finset.Ico (Order.succ a) b) = Finset.Ico a b
Finset.insert_Ioc_succ_left_eq_Ioc 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a < b) : insert (Order.succ a) (Finset.Ioc (Order.succ a) b) = Finset.Ioc a b
Finset.insert_Ico_right_eq_Ico_succ 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) : insert b (Finset.Ico a b) = Finset.Ico a (Order.succ b)
Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) : insert b (Finset.Ico a b) = Finset.Ico a (Order.succ b)
Finset.insert_Icc_right_eq_Icc_succ 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ Order.succ b) : insert (Order.succ b) (Finset.Icc a b) = Finset.Icc a (Order.succ b)
Finset.insert_Ioc_right_eq_Ioc_succ 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} [NoMaxOrder α] (h : a ≤ b) : insert (Order.succ b) (Finset.Ioc a b) = Finset.Ioc a (Order.succ b)
Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax 📋 Mathlib.Order.Interval.Finset.SuccPred
{α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [SuccOrder α] {a b : α} (h : a ≤ b) (hb : ¬IsMax b) : insert (Order.succ b) (Finset.Ioc a b) = Finset.Ioc a (Order.succ b)
IsSuccArchimedean.exists_succ_iterate_of_le 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {inst✝ : Preorder α} {inst✝¹ : SuccOrder α} [self : IsSuccArchimedean α] {a b : α} (h : a ≤ b) : ∃ n, Order.succ^[n] a = b
IsSuccArchimedean.mk 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} [Preorder α] [SuccOrder α] (exists_succ_iterate_of_le : ∀ {a b : α}, a ≤ b → ∃ n, Order.succ^[n] a = b) : IsSuccArchimedean α
LE.le.exists_succ_iterate 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a b : α} (h : a ≤ b) : ∃ n, Order.succ^[n] a = b
exists_succ_iterate_iff_le 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {a b : α} : (∃ n, Order.succ^[n] a = b) ↔ a ≤ b
Succ.rec_iff 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (Order.succ a)) {a b : α} (h : a ≤ b) : p a ↔ p b
Succ.rec_bot 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [IsSuccArchimedean α] (p : α → Prop) (hbot : p ⊥) (hsucc : ∀ (a : α), p a → p (Order.succ a)) (a : α) : p a
antitone_of_succ_le 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f (Order.succ a) ≤ f a) : Antitone f
monotone_of_le_succ 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f a ≤ f (Order.succ a)) : Monotone f
strictAnti_of_succ_lt 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f (Order.succ a) < f a) : StrictAnti f
strictMono_of_lt_succ 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {f : α → β} (hf : ∀ (a : α), ¬IsMax a → f a < f (Order.succ a)) : StrictMono f
Succ.rec_linear 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {p : α → Prop} (hsucc : ∀ (a : α), p a ↔ p (Order.succ a)) (a b : α) : p a ↔ p b
Succ.rec 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] {m : α} {P : (n : α) → m ≤ n → Prop} (rfl : P m ⋯) (succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯) ⦃n : α⦄ (hmn : m ≤ n) : P n hmn
exists_succ_iterate_or 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] {a b : α} : (∃ n, Order.succ^[n] a = b) ∨ ∃ n, Order.succ^[n] b = a
antitoneOn_of_succ_le 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) ≤ f a) : AntitoneOn f s
monotoneOn_of_le_succ 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a ≤ f (Order.succ a)) : MonotoneOn f s
strictAntiOn_of_succ_lt 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) < f a) : StrictAntiOn f s
strictMonoOn_of_lt_succ 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_3} {β : Type u_4} [PartialOrder α] [Preorder β] [SuccOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β} (hs : s.OrdConnected) (hf : ∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f a < f (Order.succ a)) : StrictMonoOn f s
succ_max 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [LinearOrder α] [SuccOrder α] (a b : α) : Order.succ (max a b) = max (Order.succ a) (Order.succ b)
succ_min 📋 Mathlib.Order.SuccPred.Archimedean
{α : Type u_1} [LinearOrder α] [SuccOrder α] (a b : α) : Order.succ (min a b) = min (Order.succ a) (Order.succ b)
Order.not_isSuccLimit_succ 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : ¬Order.IsSuccLimit (Order.succ a)
Order.IsSuccLimit.isMax 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : Order.IsSuccLimit (Order.succ a)) : IsMax a
Order.not_isSuccLimit_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) : ¬Order.IsSuccLimit (Order.succ a)
Order.not_isSuccPrelimit_succ 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : ¬Order.IsSuccPrelimit (Order.succ a)
Order.IsSuccPrelimit.isMax 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : Order.IsSuccPrelimit (Order.succ a)) : IsMax a
Order.not_isSuccPrelimit_succ_of_not_isMax 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) : ¬Order.IsSuccPrelimit (Order.succ a)
Order.IsSuccLimit.succ_ne 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccLimit a) (b : α) : Order.succ b ≠ a
Order.IsSuccPrelimit.succ_ne 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccPrelimit a) (b : α) : Order.succ b ≠ a
Order.isSuccPrelimit_of_succ_ne 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ∀ (b : α), Order.succ b ≠ a) : Order.IsSuccPrelimit a
Order.mem_range_succ_of_not_isSuccPrelimit 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ¬Order.IsSuccPrelimit a) : a ∈ Set.range Order.succ
Order.mem_range_succ_or_isSuccPrelimit 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) : a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a
Order.isSuccPrelimit_iff_succ_ne 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] : Order.IsSuccPrelimit a ↔ ∀ (b : α), Order.succ b ≠ a
Order.IsSuccLimit.succ_lt 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) (ha : a < b) : Order.succ a < b
Order.isMin_or_mem_range_succ_or_isSuccLimit 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) : IsMin a ∨ a ∈ Set.range Order.succ ∨ Order.IsSuccLimit a
Order.IsSuccLimit.succ_lt_iff 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) : Order.succ a < b ↔ a < b
Order.isSuccPrelimitRecOn 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} (b : α) {motive : α → Sort u_2} [PartialOrder α] [SuccOrder α] (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a) : motive b
Order.isSuccPrelimit_of_succ_lt 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] (H : ∀ a < b, Order.succ a < b) : Order.IsSuccPrelimit b
Order.not_isSuccPrelimit_iff 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] : ¬Order.IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ Order.succ b = a
Order.not_isSuccPrelimit_iff' 📋 Mathlib.Order.SuccPred.Limit
{α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] : ¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision 519f454