mathlib documentation

order.succ_pred.relation

Relations on types with a succ_order #

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

theorem refl_trans_gen_of_succ_of_le {α : Type u_1} [partial_order α] [succ_order α] [is_succ_archimedean α] (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 refl_trans_gen_of_succ_of_ge {α : Type u_1} [partial_order α] [succ_order α] [is_succ_archimedean α] (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 trans_gen_of_succ_of_lt {α : Type u_1} [partial_order α] [succ_order α] [is_succ_archimedean α] (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 trans_gen_of_succ_of_gt {α : Type u_1} [partial_order α] [succ_order α] [is_succ_archimedean α] (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 refl_trans_gen_of_succ {α : Type u_1} [linear_order α] [succ_order α] [is_succ_archimedean α] (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 trans_gen_of_succ_of_ne {α : Type u_1} [linear_order α] [succ_order α] [is_succ_archimedean α] (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 trans_gen_of_succ_of_reflexive {α : Type u_1} [linear_order α] [succ_order α] [is_succ_archimedean α] (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 refl_trans_gen_of_pred_of_ge {α : Type u_1} [partial_order α] [pred_order α] [is_pred_archimedean α] (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 refl_trans_gen_of_pred_of_le {α : Type u_1} [partial_order α] [pred_order α] [is_pred_archimedean α] (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 trans_gen_of_pred_of_gt {α : Type u_1} [partial_order α] [pred_order α] [is_pred_archimedean α] (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 trans_gen_of_pred_of_lt {α : Type u_1} [partial_order α] [pred_order α] [is_pred_archimedean α] (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 refl_trans_gen_of_pred {α : Type u_1} [linear_order α] [pred_order α] [is_pred_archimedean α] (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 trans_gen_of_pred_of_ne {α : Type u_1} [linear_order α] [pred_order α] [is_pred_archimedean α] (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 trans_gen_of_pred_of_reflexive {α : Type u_1} [linear_order α] [pred_order α] [is_pred_archimedean α] (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.