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 m → r i (Order.succ i)) (hnm : n ≤ m) : Relation.ReflTransGen r 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 n → r (Order.succ i) i) (hmn : m ≤ n) : Relation.ReflTransGen r n m

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 m → r i (Order.succ i)) (hnm : n < m) : Relation.TransGen r 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 n → r (Order.succ i) i) (hmn : m < n) : Relation.TransGen r n m

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 m → r i (Order.succ i)) (h2 : (i : α) → i ∈ Set.Ico m n → r (Order.succ i) i) : Relation.ReflTransGen r n m

(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 m → r i (Order.succ i)) (h2 : (i : α) → i ∈ Set.Ico m n → r (Order.succ i) i) (hnm : n ≠ m) : Relation.TransGen r 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 m → r i (Order.succ i)) (h2 : (i : α) → i ∈ Set.Ico m n → r (Order.succ i) i) : Relation.TransGen r n m

(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 n → r i (Order.pred i)) (hnm : m ≤ n) : Relation.ReflTransGen r n m

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 m → r (Order.pred i) i) (hmn : n ≤ m) : Relation.ReflTransGen r 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 n → r i (Order.pred i)) (hnm : m < n) : Relation.TransGen r n m

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 m → r (Order.pred i) i) (hmn : n < m) : Relation.TransGen r 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 n → r i (Order.pred i)) (h2 : (i : α) → i ∈ Set.Ioc n m → r (Order.pred i) i) : Relation.ReflTransGen r n m

(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 n → r i (Order.pred i)) (h2 : (i : α) → i ∈ Set.Ioc n m → r (Order.pred i) i) (hnm : n ≠ m) : Relation.TransGen r 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 n → r i (Order.pred i)) (h2 : (i : α) → i ∈ Set.Ioc n m → r (Order.pred i) i) : Relation.TransGen r n m

(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.