# 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico n mr i ()) (hnm : n m) :

For n ≤ m≤ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico m nr () i) (hmn : m n) :

For m ≤ n≤ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico n mr 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ico m nr () 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ico n mr i ()) (h2 : (i : α) → i Set.Ico m nr () 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ico n mr i ()) (h2 : (i : α) → i Set.Ico m nr () i) (hnm : n m) :

For n ≠ m≠ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (hr : ) (h1 : (i : α) → i Set.Ico n mr i ()) (h2 : (i : α) → i Set.Ico m nr () 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc m nr i ()) (hnm : m n) :

For m ≤ n≤ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc n mr () i) (hmn : n m) :

For n ≤ m≤ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h : (i : α) → i Set.Ioc m nr i ()) (hnm : m < n) :

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

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

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

theorem reflTransGen_of_pred {α : Type u_1} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ioc m nr i ()) (h2 : (i : α) → i Set.Ioc n mr () 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (h1 : (i : α) → i Set.Ioc m nr i ()) (h2 : (i : α) → i Set.Ioc n mr () i) (hnm : n m) :

For n ≠ m≠ 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} [inst : ] [inst : ] [inst : ] (r : ααProp) {n : α} {m : α} (hr : ) (h1 : (i : α) → i Set.Ioc m nr i ()) (h2 : (i : α) → i Set.Ioc n mr () 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.