Mathlib.Order.SuccPred.Relation

reflTransGen_of_succ_of_le theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i)) (hnm : n ≤ m) : ReflTransGen r n m

Full source

/-- 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_le (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i))
    (hnm : n ≤ m) : ReflTransGen r n m := by
  revert h; refine Succ.rec ?_ ?_ hnm
  · intro _
    exact ReflTransGen.refl
  · intro m hnm ih h
    have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
    rcases (le_succ m).eq_or_lt with hm | hm
    · rwa [← hm]
    exact this.tail (h m ⟨hnm, hm⟩)

Reflexive-Transitive Closure via Successor Relation on Interval

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $n \leq m$, if for every $i$ in the interval $[n, m)$ we have $r(i, \text{succ}(i))$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

reflTransGen_of_succ_of_ge theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i) (hmn : m ≤ n) : ReflTransGen r n m

Full source

/-- For `m ≤ n`, `(n, m)` is in the reflexive-transitive closure of `~` if `succ i ~ i`
  for all `i` between `n` and `m`. -/
theorem reflTransGen_of_succ_of_ge (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i)
    (hmn : m ≤ n) : ReflTransGen r n m := by
  rw [← reflTransGen_swap]
  exact reflTransGen_of_succ_of_le (swap r) h hmn

Reflexive-Transitive Closure via Predecessor Relation on Interval

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $m \leq n$, if for every $i$ in the interval $[m, n)$ we have $r(\text{succ}(i), i)$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

transGen_of_succ_of_lt theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i)) (hnm : n < m) : TransGen r n m

Full source

/-- 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_lt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico n m, r i (succ i))
    (hnm : n < m) : TransGen r n m :=
  (reflTransGen_iff_eq_or_transGen.mp <| reflTransGen_of_succ_of_le r h hnm.le).resolve_left
    hnm.ne'

Transitive Closure via Successor Relation on Strictly Ordered Interval

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $n < m$, if for every $i$ in the interval $[n, m)$ we have $r(i, \text{succ}(i))$, then $(n, m)$ is in the transitive closure of $r$.

transGen_of_succ_of_gt theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i) (hmn : m < n) : TransGen r n m

Full source

/-- 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 transGen_of_succ_of_gt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ico m n, r (succ i) i)
    (hmn : m < n) : TransGen r n m :=
  (reflTransGen_iff_eq_or_transGen.mp <| reflTransGen_of_succ_of_ge r h hmn.le).resolve_left
    hmn.ne

Transitive Closure via Predecessor Relation on Strictly Ordered Interval

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $m < n$, if for every $i$ in the interval $[m, n)$ we have $r(\text{succ}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.

reflTransGen_of_succ theorem

 (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i)) (h2 : ∀ i ∈ Ico m n, r (succ i) i) : ReflTransGen r n m

Full source

/-- `(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 reflTransGen_of_succ (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i))
    (h2 : ∀ i ∈ Ico m n, r (succ i) i) : ReflTransGen r n m :=
  (le_total n m).elim (reflTransGen_of_succ_of_le r h1) <| reflTransGen_of_succ_of_ge r h2

Reflexive-Transitive Closure via Successor and Predecessor Relations on Interval

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$, if for every $i$ in the interval $[n, m)$ we have $r(i, \text{succ}(i))$, and for every $i$ in the interval $[m, n)$ we have $r(\text{succ}(i), i)$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

transGen_of_succ_of_ne theorem

 (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i)) (h2 : ∀ i ∈ Ico m n, r (succ i) i) (hnm : n ≠ m) :
  TransGen r n m

Full source

/-- 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_ne (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i))
    (h2 : ∀ i ∈ Ico m n, r (succ i) i) (hnm : n ≠ m) : TransGen r n m :=
  (reflTransGen_iff_eq_or_transGen.mp (reflTransGen_of_succ r h1 h2)).resolve_left hnm.symm

Transitive Closure via Successor and Predecessor Relations on Interval for Distinct Elements

Informal description

Let $\alpha$ be a type with a successor order, and let $r$ be a binary relation on $\alpha$. For any two distinct elements $n, m \in \alpha$, if for every $i$ in the interval $[n, m)$ we have $r(i, \text{succ}(i))$, and for every $i$ in the interval $[m, n)$ we have $r(\text{succ}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.

transGen_of_succ_of_reflexive theorem

 (r : α → α → Prop) {n m : α} (hr : Reflexive r) (h1 : ∀ i ∈ Ico n m, r i (succ i)) (h2 : ∀ i ∈ Ico m n, r (succ i) i) :
  TransGen r n m

Full source

/-- `(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 transGen_of_succ_of_reflexive (r : α → α → Prop) {n m : α} (hr : Reflexive r)
    (h1 : ∀ i ∈ Ico n m, r i (succ i)) (h2 : ∀ i ∈ Ico m n, r (succ i) i) : TransGen r n m := by
  rcases eq_or_ne m n with (rfl | hmn); · exact TransGen.single (hr m)
  exact transGen_of_succ_of_ne r h1 h2 hmn.symm

Transitive Closure via Successor Relations for Reflexive Relations

Informal description

Let $\alpha$ be a type equipped with a successor order, and let $r$ be a reflexive binary relation on $\alpha$. For any two elements $n, m \in \alpha$, if for every $i$ in the interval $[n, m)$ we have $r(i, \text{succ}(i))$, and for every $i$ in the interval $[m, n)$ we have $r(\text{succ}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.

reflTransGen_of_pred_of_ge theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i)) (hnm : m ≤ n) : ReflTransGen r n m

Full source

/-- 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_ge (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i))
    (hnm : m ≤ n) : ReflTransGen r n m :=
  reflTransGen_of_succ_of_le (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm

Reflexive-Transitive Closure via Predecessor Relation on Reverse Interval

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $m \leq n$, if for every $i$ in the interval $(m, n]$ we have $r(i, \text{pred}(i))$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

reflTransGen_of_pred_of_le theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc n m, r (pred i) i) (hmn : n ≤ m) : ReflTransGen r n m

Full source

/-- For `n ≤ m`, `(n, m)` is in the reflexive-transitive closure of `~` if `pred i ~ i`
  for all `i` between `n` and `m`. -/
theorem reflTransGen_of_pred_of_le (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc n m, r (pred i) i)
    (hmn : n ≤ m) : ReflTransGen r n m :=
  reflTransGen_of_succ_of_ge (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hmn

Reflexive-Transitive Closure via Predecessor Relation on Right-Half-Open Interval

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $n \leq m$, if for every $i$ in the interval $(n, m]$ we have $r(\text{pred}(i), i)$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

transGen_of_pred_of_gt theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i)) (hnm : m < n) : TransGen r n m

Full source

/-- 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_gt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc m n, r i (pred i))
    (hnm : m < n) : TransGen r n m :=
  transGen_of_succ_of_lt (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm

Transitive Closure via Predecessor Relation on Strictly Ordered Reverse Interval

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $m < n$, if for every $i$ in the interval $(m, n]$ we have $r(i, \text{pred}(i))$, then $(n, m)$ is in the transitive closure of $r$.

transGen_of_pred_of_lt theorem

(r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc n m, r (pred i) i) (hmn : n < m) : TransGen r n m

Full source

/-- 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 transGen_of_pred_of_lt (r : α → α → Prop) {n m : α} (h : ∀ i ∈ Ioc n m, r (pred i) i)
    (hmn : n < m) : TransGen r n m :=
  transGen_of_succ_of_gt (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hmn

Transitive Closure via Predecessor Relation on Left-Half-Open Interval

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$ with $n < m$, if for every $i$ in the interval $(n, m]$ we have $r(\text{pred}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.

reflTransGen_of_pred theorem

 (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i)) (h2 : ∀ i ∈ Ioc n m, r (pred i) i) : ReflTransGen r n m

Full source

/-- `(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 reflTransGen_of_pred (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i))
    (h2 : ∀ i ∈ Ioc n m, r (pred i) i) : ReflTransGen r n m :=
  reflTransGen_of_succ (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩) fun x hx =>
    h2 x ⟨hx.2, hx.1⟩

Reflexive-Transitive Closure via Predecessor Relations on Intervals

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two elements $n, m \in \alpha$, if for every $i$ in the interval $(m, n]$ we have $r(i, \text{pred}(i))$, and for every $i$ in the interval $(n, m]$ we have $r(\text{pred}(i), i)$, then $(n, m)$ is in the reflexive-transitive closure of $r$.

transGen_of_pred_of_ne theorem

 (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i)) (h2 : ∀ i ∈ Ioc n m, r (pred i) i) (hnm : n ≠ m) :
  TransGen r n m

Full source

/-- 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_ne (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ioc m n, r i (pred i))
    (h2 : ∀ i ∈ Ioc n m, r (pred i) i) (hnm : n ≠ m) : TransGen r n m :=
  transGen_of_succ_of_ne (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩)
    (fun x hx => h2 x ⟨hx.2, hx.1⟩) hnm

Transitive Closure via Predecessor Relations on Intervals for Distinct Elements

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a binary relation on $\alpha$. For any two distinct elements $n, m \in \alpha$, if for every $i$ in the interval $(m, n]$ we have $r(i, \text{pred}(i))$, and for every $i$ in the interval $(n, m]$ we have $r(\text{pred}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.

transGen_of_pred_of_reflexive theorem

 (r : α → α → Prop) {n m : α} (hr : Reflexive r) (h1 : ∀ i ∈ Ioc m n, r i (pred i)) (h2 : ∀ i ∈ Ioc n m, r (pred i) i) :
  TransGen r n m

Full source

/-- `(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`. -/
theorem transGen_of_pred_of_reflexive (r : α → α → Prop) {n m : α} (hr : Reflexive r)
    (h1 : ∀ i ∈ Ioc m n, r i (pred i)) (h2 : ∀ i ∈ Ioc n m, r (pred i) i) : TransGen r n m :=
  transGen_of_succ_of_reflexive (α := αᵒᵈ) r hr (fun x hx => h1 x ⟨hx.2, hx.1⟩) fun x hx =>
    h2 x ⟨hx.2, hx.1⟩

Transitive Closure via Predecessor Relations for Reflexive Relations

Informal description

Let $\alpha$ be a type with a predecessor order, and let $r$ be a reflexive binary relation on $\alpha$. For any two elements $n, m \in \alpha$, if for every $i$ in the interval $(m, n]$ we have $r(i, \text{pred}(i))$, and for every $i$ in the interval $(n, m]$ we have $r(\text{pred}(i), i)$, then $(n, m)$ is in the transitive closure of $r$.