mathlib3 documentation

order.succ_pred.relation

Relations on types with a succ_order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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 m → r i (order.succ i)) (hnm : n ≤ m) :
relation.refl_trans_gen 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.

source
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 n → r (order.succ i) i) (hmn : m ≤ n) :
relation.refl_trans_gen 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.

source
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 m → r i (order.succ i)) (hnm : n < m) :
relation.trans_gen 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.

source
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 n → r (order.succ i) i) (hmn : m < n) :
relation.trans_gen 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.

source
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 m → r i (order.succ i)) (h2 : ∀ (i : α), i ∈ set.Ico m n → r (order.succ i) i) :
relation.refl_trans_gen 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.

source
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 m → r i (order.succ i)) (h2 : ∀ (i : α), i ∈ set.Ico m n → r (order.succ i) i) (hnm : n ≠ m) :
relation.trans_gen 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.

source
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 m → r i (order.succ i)) (h2 : ∀ (i : α), i ∈ set.Ico m n → r (order.succ i) i) :
relation.trans_gen 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.

source
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 n → r i (order.pred i)) (hnm : m ≤ n) :
relation.refl_trans_gen 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.

source
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 m → r (order.pred i) i) (hmn : n ≤ m) :
relation.refl_trans_gen 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.

source
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 n → r i (order.pred i)) (hnm : m < n) :
relation.trans_gen 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.

source
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 m → r (order.pred i) i) (hmn : n < m) :
relation.trans_gen 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.

source
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 n → r i (order.pred i)) (h2 : ∀ (i : α), i ∈ set.Ioc n m → r (order.pred i) i) :
relation.refl_trans_gen 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.

source
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 n → r i (order.pred i)) (h2 : ∀ (i : α), i ∈ set.Ioc n m → r (order.pred i) i) (hnm : n ≠ m) :
relation.trans_gen 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.

source
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 n → r i (order.pred i)) (h2 : ∀ (i : α), i ∈ set.Ioc n m → r (order.pred i) i) :
relation.trans_gen 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.