Documentation

Mathlib.Order.SuccPred.Relation

Relations on types with a SuccOrder #

This file contains properties about relations on types with a SuccOrder and their closure operations (like the transitive closure).

theorem reflTransGen_of_succ_of_le {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico n mr i (Order.succ i)) (hnm : n m) :

For n ≤ m, (n, m) is in the reflexive-transitive closure of ~ if i ~ succ i for all i between n and m.

theorem reflTransGen_of_succ_of_ge {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico m nr (Order.succ i) i) (hmn : m n) :

For m ≤ n, (n, m) is in the reflexive-transitive closure of ~ if succ i ~ i for all i between n and m.

theorem transGen_of_succ_of_lt {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico n mr i (Order.succ i)) (hnm : n < m) :

For n < m, (n, m) is in the transitive closure of a relation ~ if i ~ succ i for all i between n and m.

theorem transGen_of_succ_of_gt {α : Type u_1} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico m nr (Order.succ i) i) (hmn : m < n) :

For m < n, (n, m) is in the transitive closure of a relation ~ if succ i ~ i for all i between n and m.

theorem reflTransGen_of_succ {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ico n mr i (Order.succ i)) (h2 : (i : α) → i Set.Ico m nr (Order.succ i) i) :

(n, m) is in the reflexive-transitive closure of ~ if i ~ succ i and succ i ~ i for all i between n and m.

theorem transGen_of_succ_of_ne {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ico n mr i (Order.succ i)) (h2 : (i : α) → i Set.Ico m nr (Order.succ i) i) (hnm : n m) :

For n ≠ m,(n, m) is in the transitive closure of a relation ~ if i ~ succ i and succ i ~ i for all i between n and m.

theorem transGen_of_succ_of_reflexive {α : Type u_1} [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] (r : ααProp) {n : α} {m : α} (hr : Reflexive r) (h1 : (i : α) → i Set.Ico n mr i (Order.succ i)) (h2 : (i : α) → i Set.Ico m nr (Order.succ i) i) :

(n, m) is in the transitive closure of a reflexive relation ~ if i ~ succ i and succ i ~ i for all i between n and m.

theorem reflTransGen_of_pred_of_ge {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc m nr i (Order.pred i)) (hnm : m n) :

For m ≤ n, (n, m) is in the reflexive-transitive closure of ~ if i ~ pred i for all i between n and m.

theorem reflTransGen_of_pred_of_le {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc n mr (Order.pred i) i) (hmn : n m) :

For n ≤ m, (n, m) is in the reflexive-transitive closure of ~ if pred i ~ i for all i between n and m.

theorem transGen_of_pred_of_gt {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc m nr i (Order.pred i)) (hnm : m < n) :

For m < n, (n, m) is in the transitive closure of a relation ~ for n ≠ m if i ~ pred i for all i between n and m.

theorem transGen_of_pred_of_lt {α : Type u_1} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc n mr (Order.pred i) i) (hmn : n < m) :

For n < m, (n, m) is in the transitive closure of a relation ~ for n ≠ m if pred i ~ i for all i between n and m.

theorem reflTransGen_of_pred {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ioc m nr i (Order.pred i)) (h2 : (i : α) → i Set.Ioc n mr (Order.pred i) i) :

(n, m) is in the reflexive-transitive closure of ~ if i ~ pred i and pred i ~ i for all i between n and m.

theorem transGen_of_pred_of_ne {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ioc m nr i (Order.pred i)) (h2 : (i : α) → i Set.Ioc n mr (Order.pred i) i) (hnm : n m) :

For n ≠ m, (n, m) is in the transitive closure of a relation ~ if i ~ pred i and pred i ~ i for all i between n and m.

theorem transGen_of_pred_of_reflexive {α : Type u_1} [LinearOrder α] [PredOrder α] [IsPredArchimedean α] (r : ααProp) {n : α} {m : α} (hr : Reflexive r) (h1 : (i : α) → i Set.Ioc m nr i (Order.pred i)) (h2 : (i : α) → i Set.Ioc n mr (Order.pred i) i) :

(n, m) is in the transitive closure of a reflexive relation ~ if i ~ pred i and pred i ~ i for all i between n and m.