Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov

! This file was ported from Lean 3 source module order.iterate
! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Function.Iterate
import Mathlib.Order.Monotone.Basic

/-!
# Inequalities on iterates

In this file we prove some inequalities comparing `f^[n] x` and `g^[n] x` where `f` and `g` are
two self-maps that commute with each other.

Current selection of inequalities is motivated by formalization of the rotation number of
a circle homeomorphism.
-/


open Function

namespace Monotone

variable [
Preorder: Type ?u.2419 β†’ Type ?u.2419
Preorder 
Ξ±: ?m.24
Ξ±] {
f: Ξ± β†’ Ξ±
f : 
Ξ±: ?m.483
Ξ± β†’ 
Ξ±: ?m.2396
Ξ±} {
x: β„• β†’ Ξ±
x 
y: β„• β†’ Ξ±
y : 
β„•: Type
β„• β†’ 
Ξ±: ?m.4
Ξ±}

/-!
### Comparison of two sequences

If $f$ is a monotone function, then $βˆ€ k, x_{k+1} ≀ f(x_k)$ implies that $x_k$ grows slower than
$f^k(x_0)$, and similarly for the reversed inequalities. If $x_k$ and $y_k$ are two sequences such
that $x_{k+1} ≀ f(x_k)$ and $y_{k+1} β‰₯ f(y_k)$ for all $k < n$, then $x_0 ≀ y_0$ implies
$x_n ≀ y_n$, see `Monotone.seq_le_seq`.

If some of the inequalities in this lemma are strict, then we have $x_n < y_n$. The rest of the
lemmas in this section formalize this fact for different inequalities made strict.
-/


theorem 
seq_le_seq: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ (n : β„•),
      x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n
seq_le_seq (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.43} β†’ {Ξ² : Type ?u.42} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
n: β„•
n : 
β„•: Type
β„•) (
hβ‚€: x 0 ≀ y 0
hβ‚€ : 
x: β„• β†’ Ξ±
x 
0: ?m.78
0 ≀ 
y: β„• β†’ Ξ±
y 
0: ?m.89
0) (
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
hx : βˆ€ 
k: ?m.104
k < 
n: β„•
n, 
x: β„• β†’ Ξ±
x (
k: ?m.104
k + 
1: ?m.120
1) ≀ 
f: Ξ± β†’ Ξ±
f (
x: β„• β†’ Ξ±
x 
k: ?m.104
k))
    (
hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)
hy : βˆ€ 
k: ?m.181
k < 
n: β„•
n, 
f: Ξ± β†’ Ξ±
f (
y: β„• β†’ Ξ±
y 
k: ?m.181
k) ≀ 
y: β„• β†’ Ξ±
y (
k: ?m.181
k + 
1: ?m.194
1)) : 
x: β„• β†’ Ξ±
x 
n: β„•
n ≀ 
y: β„• β†’ Ξ±
y 
n: β„•
n := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero ≀ y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero ≀ y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero ≀ y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ.refine'_1
βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ.refine'_2
βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ.refine'_2
βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) ≀ f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) ≀ f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) ≀ y (Nat.succ n)
Goals accomplished! πŸ™

#align monotone.seq_le_seq 
Monotone.seq_le_seq: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ (n : β„•),
      x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n ≀ y n
Monotone.seq_le_seq

theorem 
seq_pos_lt_seq_of_lt_of_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ {n : β„•},
      0 < n β†’
        x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
seq_pos_lt_seq_of_lt_of_le (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.502} β†’ {Ξ² : Type ?u.501} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) {
n: β„•
n : 
β„•: Type
β„•} (
hn: 0 < n
hn : 
0: ?m.537
0 < 
n: β„•
n) (
hβ‚€: x 0 ≀ y 0
hβ‚€ : 
x: β„• β†’ Ξ±
x 
0: ?m.574
0 ≀ 
y: β„• β†’ Ξ±
y 
0: ?m.577
0)
    (
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)
hx : βˆ€ 
k: ?m.592
k < 
n: β„•
n, 
x: β„• β†’ Ξ±
x (
k: ?m.592
k + 
1: ?m.605
1) < 
f: Ξ± β†’ Ξ±
f (
x: β„• β†’ Ξ±
x 
k: ?m.592
k)) (
hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)
hy : βˆ€ 
k: ?m.673
k < 
n: β„•
n, 
f: Ξ± β†’ Ξ±
f (
y: β„• β†’ Ξ±
y 
k: ?m.673
k) ≀ 
y: β„• β†’ Ξ±
y (
k: ?m.673
k + 
1: ?m.686
1)) : 
x: β„• β†’ Ξ±
x 
n: β„•
n < 
y: β„• β†’ Ξ±
y 
n: β„•
n := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn: 0 < n

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn✝: 0 < n

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hn: 0 < Nat.zero

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero < y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < n β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n

hn: 0 < Nat.succ n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) < y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn: 0 < n

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn✝: 0 < n

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hn: 0 < Nat.zero

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero < y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn✝: 0 < n

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

hn: 0 < Nat.zero

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero < y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < n β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n

hn: 0 < Nat.succ n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n) < y (Nat.succ n)
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn: 0 < n

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < n β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n

hn: 0 < Nat.succ n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn: 0 < n

hβ‚€: x 0 ≀ y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < n β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n

hn: 0 < Nat.succ n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hn✝: 0 < n

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

ihn: 0 < Nat.zero β†’
  (βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)) β†’ x Nat.zero < y Nat.zero

hn: 0 < Nat.succ Nat.zero

hx: βˆ€ (k : β„•), k < Nat.succ Nat.zero β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ Nat.zero β†’ f (y k) ≀ y (k + 1)

succ.zero
x Nat.zero ≀ y Nat.zero
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < n β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n

hn: 0 < Nat.succ n

hx: βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)

succ
x n ≀ y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

succ.succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

k: β„•

hk: k < Nat.succ n

succ.succ.refine'_1
k < Nat.succ (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

k: β„•

hk: k < Nat.succ n

succ.succ.refine'_2
k < Nat.succ (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

succ.succ
x (Nat.succ n) ≀ y (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

k: β„•

hk: k < Nat.succ n

succ.succ.refine'_1
k < Nat.succ (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

k: β„•

hk: k < Nat.succ n

succ.succ.refine'_2
k < Nat.succ (Nat.succ n)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n✝: β„•

hn✝: 0 < n✝

hβ‚€: x 0 ≀ y 0

hx✝: βˆ€ (k : β„•), k < n✝ β†’ x (k + 1) < f (x k)

hy✝: βˆ€ (k : β„•), k < n✝ β†’ f (y k) ≀ y (k + 1)

n: β„•

ihn: 0 < Nat.succ n β†’
  (βˆ€ (k : β„•), k < Nat.succ n β†’ x (k + 1) < f (x k)) β†’
    (βˆ€ (k : β„•), k < Nat.succ n β†’ f (y k) ≀ y (k + 1)) β†’ x (Nat.succ n) < y (Nat.succ n)

hn: 0 < Nat.succ (Nat.succ n)

hx: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ (Nat.succ n) β†’ f (y k) ≀ y (k + 1)

succ.succ
x (Nat.succ n) ≀ y (Nat.succ n)
Goals accomplished! πŸ™

#align monotone.seq_pos_lt_seq_of_lt_of_le 
Monotone.seq_pos_lt_seq_of_lt_of_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ {n : β„•},
      0 < n β†’
        x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
Monotone.seq_pos_lt_seq_of_lt_of_le

theorem 
seq_pos_lt_seq_of_le_of_lt: Monotone f β†’
  βˆ€ {n : β„•},
    0 < n β†’ x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)) β†’ x n < y n
seq_pos_lt_seq_of_le_of_lt (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.1229} β†’ {Ξ² : Type ?u.1228} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) {
n: β„•
n : 
β„•: Type
β„•} (
hn: 0 < n
hn : 
0: ?m.1264
0 < 
n: β„•
n) (
hβ‚€: x 0 ≀ y 0
hβ‚€ : 
x: β„• β†’ Ξ±
x 
0: ?m.1301
0 ≀ 
y: β„• β†’ Ξ±
y 
0: ?m.1304
0)
    (
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
hx : βˆ€ 
k: ?m.1319
k < 
n: β„•
n, 
x: β„• β†’ Ξ±
x (
k: ?m.1319
k + 
1: ?m.1332
1) ≀ 
f: Ξ± β†’ Ξ±
f (
x: β„• β†’ Ξ±
x 
k: ?m.1319
k)) (
hy: βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)
hy : βˆ€ 
k: ?m.1393
k < 
n: β„•
n, 
f: Ξ± β†’ Ξ±
f (
y: β„• β†’ Ξ±
y 
k: ?m.1393
k) < 
y: β„• β†’ Ξ±
y (
k: ?m.1393
k + 
1: ?m.1406
1)) : 
x: β„• β†’ Ξ±
x 
n: β„•
n < 
y: β„• β†’ Ξ±
y 
n: β„•
n :=
  
hf: Monotone f
hf.
dual: βˆ€ {Ξ± : Type ?u.1475} {Ξ² : Type ?u.1474} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.
seq_pos_lt_seq_of_lt_of_le: βˆ€ {Ξ± : Type ?u.1492} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ {n : β„•},
      0 < n β†’
        x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
seq_pos_lt_seq_of_lt_of_le 
hn: 0 < n
hn 
hβ‚€: x 0 ≀ y 0
hβ‚€ 
hy: βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)
hy 
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
hx
#align monotone.seq_pos_lt_seq_of_le_of_lt 
Monotone.seq_pos_lt_seq_of_le_of_lt: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ {n : β„•},
      0 < n β†’
        x 0 ≀ y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)) β†’ x n < y n
Monotone.seq_pos_lt_seq_of_le_of_lt

theorem 
seq_lt_seq_of_lt_of_le: Monotone f β†’
  βˆ€ (n : β„•), x 0 < y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
seq_lt_seq_of_lt_of_le (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.1600} β†’ {Ξ² : Type ?u.1599} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
n: β„•
n : 
β„•: Type
β„•) (
hβ‚€: x 0 < y 0
hβ‚€ : 
x: β„• β†’ Ξ±
x 
0: ?m.1635
0 < 
y: β„• β†’ Ξ±
y 
0: ?m.1646
0)
    (
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)
hx : βˆ€ 
k: ?m.1661
k < 
n: β„•
n, 
x: β„• β†’ Ξ±
x (
k: ?m.1661
k + 
1: ?m.1677
1) < 
f: Ξ± β†’ Ξ±
f (
x: β„• β†’ Ξ±
x 
k: ?m.1661
k)) (
hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)
hy : βˆ€ 
k: ?m.1738
k < 
n: β„•
n, 
f: Ξ± β†’ Ξ±
f (
y: β„• β†’ Ξ±
y 
k: ?m.1738
k) ≀ 
y: β„• β†’ Ξ±
y (
k: ?m.1738
k + 
1: ?m.1751
1)) : 
x: β„• β†’ Ξ±
x 
n: β„•
n < 
y: β„• β†’ Ξ±
y 
n: β„•
n := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 < y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

hβ‚€: x 0 < y 0

hx: βˆ€ (k : β„•), k < Nat.zero β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.zero β†’ f (y k) ≀ y (k + 1)

zero
x Nat.zero < y Nat.zero
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

hβ‚€: x 0 < y 0

n✝: β„•

hx: βˆ€ (k : β„•), k < Nat.succ n✝ β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < Nat.succ n✝ β†’ f (y k) ≀ y (k + 1)

succ
x (Nat.succ n✝) < y (Nat.succ n✝)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x, y: β„• β†’ Ξ±

hf: Monotone f

n: β„•

hβ‚€: x 0 < y 0

hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)

hy: βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)

x n < y n
Goals accomplished! πŸ™

#align monotone.seq_lt_seq_of_lt_of_le 
Monotone.seq_lt_seq_of_lt_of_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ (n : β„•),
      x 0 < y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
Monotone.seq_lt_seq_of_lt_of_le

theorem 
seq_lt_seq_of_le_of_lt: Monotone f β†’
  βˆ€ (n : β„•), x 0 < y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)) β†’ x n < y n
seq_lt_seq_of_le_of_lt (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.2042} β†’ {Ξ² : Type ?u.2041} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
n: β„•
n : 
β„•: Type
β„•) (
hβ‚€: x 0 < y 0
hβ‚€ : 
x: β„• β†’ Ξ±
x 
0: ?m.2077
0 < 
y: β„• β†’ Ξ±
y 
0: ?m.2088
0)
    (
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
hx : βˆ€ 
k: ?m.2103
k < 
n: β„•
n, 
x: β„• β†’ Ξ±
x (
k: ?m.2103
k + 
1: ?m.2119
1) ≀ 
f: Ξ± β†’ Ξ±
f (
x: β„• β†’ Ξ±
x 
k: ?m.2103
k)) (
hy: βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)
hy : βˆ€ 
k: ?m.2187
k < 
n: β„•
n, 
f: Ξ± β†’ Ξ±
f (
y: β„• β†’ Ξ±
y 
k: ?m.2187
k) < 
y: β„• β†’ Ξ±
y (
k: ?m.2187
k + 
1: ?m.2200
1)) : 
x: β„• β†’ Ξ±
x 
n: β„•
n < 
y: β„• β†’ Ξ±
y 
n: β„•
n :=
  
hf: Monotone f
hf.
dual: βˆ€ {Ξ± : Type ?u.2260} {Ξ² : Type ?u.2259} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.
seq_lt_seq_of_lt_of_le: βˆ€ {Ξ± : Type ?u.2277} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ (n : β„•),
      x 0 < y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) < f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) ≀ y (k + 1)) β†’ x n < y n
seq_lt_seq_of_lt_of_le 
n: β„•
n 
hβ‚€: x 0 < y 0
hβ‚€ 
hy: βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)
hy 
hx: βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)
hx
#align monotone.seq_lt_seq_of_le_of_lt 
Monotone.seq_lt_seq_of_le_of_lt: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {x y : β„• β†’ Ξ±},
  Monotone f β†’
    βˆ€ (n : β„•),
      x 0 < y 0 β†’ (βˆ€ (k : β„•), k < n β†’ x (k + 1) ≀ f (x k)) β†’ (βˆ€ (k : β„•), k < n β†’ f (y k) < y (k + 1)) β†’ x n < y n
Monotone.seq_lt_seq_of_le_of_lt

/-!
### Iterates of two functions

In this section we compare the iterates of a monotone function `f : Ξ± β†’ Ξ±` to iterates of any
function `g : Ξ² β†’ Ξ²`. If `h : Ξ² β†’ Ξ±` satisfies `h ∘ g ≀ f ∘ h`, then `h (g^[n] x)` grows slower
than `f^[n] (h x)`, and similarly for the reversed inequality.

Then we specialize these two lemmas to the case `Ξ² = Ξ±`, `h = id`.
-/


variable {
g: Ξ² β†’ Ξ²
g : 
Ξ²: ?m.2383
Ξ² β†’ 
Ξ²: ?m.2383
Ξ²} {
h: Ξ² β†’ Ξ±
h : 
Ξ²: ?m.2383
Ξ² β†’ 
Ξ±: ?m.2363
Ξ±}

open Function

theorem 
le_iterate_comp_of_le: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ h ∘ g ≀ f ∘ h β†’ βˆ€ (n : β„•), h ∘ g^[n] ≀ f^[n] ∘ h
le_iterate_comp_of_le (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.2443} β†’ {Ξ² : Type ?u.2442} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
H: h ∘ g ≀ f ∘ h
H : 
h: Ξ² β†’ Ξ±
h ∘ 
g: Ξ² β†’ Ξ²
g ≀ 
f: Ξ± β†’ Ξ±
f ∘ 
h: Ξ² β†’ Ξ±
h) (
n: β„•
n : 
β„•: Type
β„•) :
    
h: Ξ² β†’ Ξ±
h ∘ 
g: Ξ² β†’ Ξ²
g^[
n: β„•
n] ≀ 
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] ∘ 
h: Ξ² β†’ Ξ±
h := fun 
x: ?m.2625
x => 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hβ‚€
(h ∘ g^[0]) x ≀ (f^[0] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hx
βˆ€ (k : β„•), k < n β†’ (h ∘ g^[k + 1]) x ≀ f ((h ∘ g^[k]) x)
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hy
βˆ€ (k : β„•), k < n β†’ f ((f^[k] ∘ h) x) ≀ (f^[k + 1] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hβ‚€
(h ∘ g^[0]) x ≀ (f^[0] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hx
βˆ€ (k : β„•), k < n β†’ (h ∘ g^[k + 1]) x ≀ f ((h ∘ g^[k]) x)
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hy
βˆ€ (k : β„•), k < n β†’ f ((f^[k] ∘ h) x) ≀ (f^[k + 1] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

k✝: β„•

a✝: k✝ < n

hy
f ((f^[k✝] ∘ h) x) ≀ (f^[k✝ + 1] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

hβ‚€
(h ∘ g^[0]) x ≀ (f^[0] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

k✝: β„•

a✝: k✝ < n

hx
(h ∘ g^[k✝ + 1]) x ≀ f ((h ∘ g^[k✝]) x)
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

k✝: β„•

a✝: k✝ < n

hy
f ((f^[k✝] ∘ h) x) ≀ (f^[k✝ + 1] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

k✝: β„•

a✝: k✝ < n

hx
h (g ((g^[k✝]) x)) ≀ f (h ((g^[k✝]) x))
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

(h ∘ g^[n]) x ≀ (f^[n] ∘ h) x
Ξ±: Type u_1

Ξ²: Type u_2

inst✝: Preorder α

f: Ξ± β†’ Ξ±

x✝, y: β„• β†’ Ξ±

g: Ξ² β†’ Ξ²

h: Ξ² β†’ Ξ±

hf: Monotone f

H: h ∘ g ≀ f ∘ h

n: β„•

x: Ξ²

k✝: β„•

a✝: k✝ < n

h (g ((g^[k✝]) x)) ≀ f (h ((g^[k✝]) x))
Goals accomplished! πŸ™

#align monotone.le_iterate_comp_of_le 
Monotone.le_iterate_comp_of_le: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ h ∘ g ≀ f ∘ h β†’ βˆ€ (n : β„•), h ∘ g^[n] ≀ f^[n] ∘ h
Monotone.le_iterate_comp_of_le

theorem 
iterate_comp_le_of_le: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ f ∘ h ≀ h ∘ g β†’ βˆ€ (n : β„•), f^[n] ∘ h ≀ h ∘ g^[n]
iterate_comp_le_of_le (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.3598} β†’ {Ξ² : Type ?u.3597} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
H: f ∘ h ≀ h ∘ g
H : 
f: Ξ± β†’ Ξ±
f ∘ 
h: Ξ² β†’ Ξ±
h ≀ 
h: Ξ² β†’ Ξ±
h ∘ 
g: Ξ² β†’ Ξ²
g) (
n: β„•
n : 
β„•: Type
β„•) :
    
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] ∘ 
h: Ξ² β†’ Ξ±
h ≀ 
h: Ξ² β†’ Ξ±
h ∘ 
g: Ξ² β†’ Ξ²
g^[
n: β„•
n] :=
  
hf: Monotone f
hf.
dual: βˆ€ {Ξ± : Type ?u.3780} {Ξ² : Type ?u.3779} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.
le_iterate_comp_of_le: βˆ€ {Ξ± : Type ?u.3797} {Ξ² : Type ?u.3798} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ h ∘ g ≀ f ∘ h β†’ βˆ€ (n : β„•), h ∘ g^[n] ≀ f^[n] ∘ h
le_iterate_comp_of_le 
H: f ∘ h ≀ h ∘ g
H 
n: β„•
n
#align monotone.iterate_comp_le_of_le 
Monotone.iterate_comp_le_of_le: βˆ€ {Ξ± : Type u_1} {Ξ² : Type u_2} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ f ∘ h ≀ h ∘ g β†’ βˆ€ (n : β„•), f^[n] ∘ h ≀ h ∘ g^[n]
Monotone.iterate_comp_le_of_le

/-- If `f ≀ g` and `f` is monotone, then `f^[n] ≀ g^[n]`. -/
theorem 
iterate_le_of_le: βˆ€ {g : Ξ± β†’ Ξ±}, Monotone f β†’ f ≀ g β†’ βˆ€ (n : β„•), f^[n] ≀ g^[n]
iterate_le_of_le {
g: Ξ± β†’ Ξ±
g : 
Ξ±: ?m.3913
Ξ± β†’ 
Ξ±: ?m.3913
Ξ±} (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.3964} β†’ {Ξ² : Type ?u.3963} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
h: f ≀ g
h : 
f: Ξ± β†’ Ξ±
f ≀ 
g: Ξ± β†’ Ξ±
g) (
n: β„•
n : 
β„•: Type
β„•) : 
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] ≀ 
g: Ξ± β†’ Ξ±
g^[
n: β„•
n] :=
  
hf: Monotone f
hf.
iterate_comp_le_of_le: βˆ€ {Ξ± : Type ?u.4061} {Ξ² : Type ?u.4062} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±} {g : Ξ² β†’ Ξ²} {h : Ξ² β†’ Ξ±},
  Monotone f β†’ f ∘ h ≀ h ∘ g β†’ βˆ€ (n : β„•), f^[n] ∘ h ≀ h ∘ g^[n]
iterate_comp_le_of_le 
h: f ≀ g
h 
n: β„•
n
#align monotone.iterate_le_of_le 
Monotone.iterate_le_of_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±}, Monotone f β†’ f ≀ g β†’ βˆ€ (n : β„•), f^[n] ≀ g^[n]
Monotone.iterate_le_of_le

/-- If `f ≀ g` and `g` is monotone, then `f^[n] ≀ g^[n]`. -/
theorem 
le_iterate_of_le: βˆ€ {g : Ξ± β†’ Ξ±}, Monotone g β†’ f ≀ g β†’ βˆ€ (n : β„•), f^[n] ≀ g^[n]
le_iterate_of_le {
g: Ξ± β†’ Ξ±
g : 
Ξ±: ?m.4158
Ξ± β†’ 
Ξ±: ?m.4158
Ξ±} (
hg: Monotone g
hg : 
Monotone: {Ξ± : Type ?u.4209} β†’ {Ξ² : Type ?u.4208} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
g: Ξ± β†’ Ξ±
g) (
h: f ≀ g
h : 
f: Ξ± β†’ Ξ±
f ≀ 
g: Ξ± β†’ Ξ±
g) (
n: β„•
n : 
β„•: Type
β„•) : 
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] ≀ 
g: Ξ± β†’ Ξ±
g^[
n: β„•
n] :=
  
hg: Monotone g
hg.
dual: βˆ€ {Ξ± : Type ?u.4307} {Ξ² : Type ?u.4306} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.
iterate_le_of_le: βˆ€ {Ξ± : Type ?u.4324} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±}, Monotone f β†’ f ≀ g β†’ βˆ€ (n : β„•), f^[n] ≀ g^[n]
iterate_le_of_le 
h: f ≀ g
h 
n: β„•
n
#align monotone.le_iterate_of_le 
Monotone.le_iterate_of_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±}, Monotone g β†’ f ≀ g β†’ βˆ€ (n : β„•), f^[n] ≀ g^[n]
Monotone.le_iterate_of_le

end Monotone

/-!
### Comparison of iterations and the identity function

If $f(x) ≀ x$ for all $x$ (we express this as `f ≀ id` in the code), then the same is true for
any iterate of $f$, and similarly for the reversed inequality.
-/


namespace Function

section Preorder

variable [
Preorder: Type ?u.4730 β†’ Type ?u.4730
Preorder 
Ξ±: ?m.4727
Ξ±] {
f: Ξ± β†’ Ξ±
f : 
Ξ±: ?m.4409
Ξ± β†’ 
Ξ±: ?m.4727
Ξ±}

/-- If $x ≀ f x$ for all $x$ (we write this as `id ≀ f`), then the same is true for any iterate
`f^[n]` of `f`. -/
theorem 
id_le_iterate_of_id_le: id ≀ f β†’ βˆ€ (n : β„•), id ≀ f^[n]
id_le_iterate_of_id_le (
h: id ≀ f
h : 
id: {Ξ± : Sort ?u.4420} β†’ Ξ± β†’ Ξ±
id ≀ 
f: Ξ± β†’ Ξ±
f) (
n: β„•
n : 
β„•: Type
β„•) : 
id: {Ξ± : Sort ?u.4497} β†’ Ξ± β†’ Ξ±
id ≀ 
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

id ≀ f^[n]
Goals accomplished! πŸ™

#align function.id_le_iterate_of_id_le 
Function.id_le_iterate_of_id_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, id ≀ f β†’ βˆ€ (n : β„•), id ≀ f^[n]
Function.id_le_iterate_of_id_le

theorem 
iterate_le_id_of_le_id: f ≀ id β†’ βˆ€ (n : β„•), f^[n] ≀ id
iterate_le_id_of_le_id (
h: f ≀ id
h : 
f: Ξ± β†’ Ξ±
f ≀ 
id: {Ξ± : Sort ?u.4739} β†’ Ξ± β†’ Ξ±
id) (
n: β„•
n : 
β„•: Type
β„•) : 
f: Ξ± β†’ Ξ±
f^[
n: β„•
n] ≀ 
id: {Ξ± : Sort ?u.4822} β†’ Ξ± β†’ Ξ±
id :=
  @
id_le_iterate_of_id_le: βˆ€ {Ξ± : Type ?u.4868} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, id ≀ f β†’ βˆ€ (n : β„•), id ≀ f^[n]
id_le_iterate_of_id_le 
Ξ±: ?m.4727
Ξ±α΅’α΅ˆ _ 
f: Ξ± β†’ Ξ±
f 
h: f ≀ id
h 
n: β„•
n
#align function.iterate_le_id_of_le_id 
Function.iterate_le_id_of_le_id: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, f ≀ id β†’ βˆ€ (n : β„•), f^[n] ≀ id
Function.iterate_le_id_of_le_id

theorem 
monotone_iterate_of_id_le: id ≀ f β†’ Monotone fun m => f^[m]
monotone_iterate_of_id_le (
h: id ≀ f
h : 
id: {Ξ± : Sort ?u.4939} β†’ Ξ± β†’ Ξ±
id ≀ 
f: Ξ± β†’ Ξ±
f) : 
Monotone: {Ξ± : Type ?u.5014} β†’ {Ξ² : Type ?u.5013} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone fun 
m: ?m.5038
m => 
f: Ξ± β†’ Ξ±
f^[
m: ?m.5038
m] :=
  
monotone_nat_of_le_succ: βˆ€ {Ξ± : Type ?u.5093} [inst : Preorder Ξ±] {f : β„• β†’ Ξ±}, (βˆ€ (n : β„•), f n ≀ f (n + 1)) β†’ Monotone f
monotone_nat_of_le_succ $ fun 
n: ?m.5120
n 
x: ?m.5123
x => 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

x: Ξ±

(f^[n]) x ≀ (f^[n + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

x: Ξ±

(f^[n]) x ≀ (f^[n + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

x: Ξ±

(f^[n]) x ≀ f ((f^[n]) x)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

x: Ξ±

(f^[n]) x ≀ f ((f^[n]) x)
Ξ±: Type u_1

inst✝: Preorder α

f: Ξ± β†’ Ξ±

h: id ≀ f

n: β„•

x: Ξ±

(f^[n]) x ≀ (f^[n + 1]) x
Goals accomplished! πŸ™

#align function.monotone_iterate_of_id_le 
Function.monotone_iterate_of_id_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, id ≀ f β†’ Monotone fun m => f^[m]
Function.monotone_iterate_of_id_le

theorem 
antitone_iterate_of_le_id: f ≀ id β†’ Antitone fun m => f^[m]
antitone_iterate_of_le_id (
h: f ≀ id
h : 
f: Ξ± β†’ Ξ±
f ≀ 
id: {Ξ± : Sort ?u.5272} β†’ Ξ± β†’ Ξ±
id) : 
Antitone: {Ξ± : Type ?u.5347} β†’ {Ξ² : Type ?u.5346} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Antitone fun 
m: ?m.5371
m => 
f: Ξ± β†’ Ξ±
f^[
m: ?m.5371
m] := fun 
m: ?m.5427
m 
n: ?m.5430
n 
hmn: ?m.5433
hmn =>
  @
monotone_iterate_of_id_le: βˆ€ {Ξ± : Type ?u.5435} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, id ≀ f β†’ Monotone fun m => f^[m]
monotone_iterate_of_id_le 
Ξ±: ?m.5260
Ξ±α΅’α΅ˆ _ 
f: Ξ± β†’ Ξ±
f 
h: f ≀ id
h 
m: ?m.5427
m 
n: ?m.5430
n 
hmn: ?m.5433
hmn
#align function.antitone_iterate_of_le_id 
Function.antitone_iterate_of_le_id: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f : Ξ± β†’ Ξ±}, f ≀ id β†’ Antitone fun m => f^[m]
Function.antitone_iterate_of_le_id

end Preorder

/-!
### Iterates of commuting functions

If `f` and `g` are monotone and commute, then `f x ≀ g x` implies `f^[n] x ≀ g^[n] x`, see
`Function.Commute.iterate_le_of_map_le`. We also prove two strict inequality versions of this lemma,
as well as `iff` versions.
-/


namespace Commute

section Preorder

variable [
Preorder: Type ?u.6079 β†’ Type ?u.6079
Preorder 
Ξ±: ?m.5515
Ξ±] {
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g : 
Ξ±: ?m.5515
Ξ± β†’ 
Ξ±: ?m.5515
Ξ±}

theorem 
iterate_le_of_map_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ Monotone g β†’ βˆ€ {x : Ξ±}, f x ≀ g x β†’ βˆ€ (n : β„•), (f^[n]) x ≀ (g^[n]) x
iterate_le_of_map_le (
h: Commute f g
h : 
Commute: {Ξ± : Type ?u.5545} β†’ (Ξ± β†’ Ξ±) β†’ (Ξ± β†’ Ξ±) β†’ Prop
Commute 
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g) (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.5556} β†’ {Ξ² : Type ?u.5555} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
hg: Monotone g
hg : 
Monotone: {Ξ± : Type ?u.5588} β†’ {Ξ² : Type ?u.5587} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
g: Ξ± β†’ Ξ±
g) {
x: ?m.5616
x}
    (
hx: f x ≀ g x
hx : 
f: Ξ± β†’ Ξ±
f 
x: ?m.5616
x ≀ 
g: Ξ± β†’ Ξ±
g 
x: ?m.5616
x) (
n: β„•
n : 
β„•: Type
β„•) : (
f: Ξ± β†’ Ξ±
f^[
n: β„•
n]) 
x: ?m.5616
x ≀ (
g: Ξ± β†’ Ξ±
g^[
n: β„•
n]) 
x: ?m.5616
x := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

(f^[n]) x ≀ (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

(f^[n]) x ≀ (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

(f^[n]) x ≀ (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hx
f ((f^[k✝]) x) ≀ f ((f^[k✝]) x)
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

(f^[n]) x ≀ (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hy
f ((g^[k✝]) x) ≀ (g^[k✝ + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n, k✝: β„•

a✝: k✝ < n

hy
f ((g^[k✝]) x) ≀ (g^[k✝ + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: Monotone g

x: Ξ±

hx: f x ≀ g x

n: β„•

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) ≀ (g^[k + 1]) x
Goals accomplished! πŸ™
Goals accomplished! πŸ™

#align function.commute.iterate_le_of_map_le 
Function.Commute.iterate_le_of_map_le: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ Monotone g β†’ βˆ€ {x : Ξ±}, f x ≀ g x β†’ βˆ€ (n : β„•), (f^[n]) x ≀ (g^[n]) x
Function.Commute.iterate_le_of_map_le

theorem 
iterate_pos_lt_of_map_lt: Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±}, f x < g x β†’ βˆ€ {n : β„•}, 0 < n β†’ (f^[n]) x < (g^[n]) x
iterate_pos_lt_of_map_lt (
h: Commute f g
h : 
Commute: {Ξ± : Type ?u.6090} β†’ (Ξ± β†’ Ξ±) β†’ (Ξ± β†’ Ξ±) β†’ Prop
Commute 
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g) (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.6101} β†’ {Ξ² : Type ?u.6100} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
hg: StrictMono g
hg : 
StrictMono: {Ξ± : Type ?u.6133} β†’ {Ξ² : Type ?u.6132} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono 
g: Ξ± β†’ Ξ±
g) {
x: Ξ±
x}
    (
hx: f x < g x
hx : 
f: Ξ± β†’ Ξ±
f 
x: ?m.6161
x < 
g: Ξ± β†’ Ξ±
g 
x: ?m.6161
x) {
n: β„•
n} (
hn: 0 < n
hn : 
0: ?m.6182
0 < 
n: ?m.6177
n) : (
f: Ξ± β†’ Ξ±
f^[
n: ?m.6177
n]) 
x: ?m.6161
x < (
g: Ξ± β†’ Ξ±
g^[
n: ?m.6177
n]) 
x: ?m.6161
x := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hβ‚€
(f^[0]) x ≀ (g^[0]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hx
βˆ€ (k : β„•), k < n β†’ (f^[k + 1]) x ≀ f ((f^[k]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hx
(f^[k✝ + 1]) x ≀ f ((f^[k✝]) x)
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hx
f ((f^[k✝]) x) ≀ f ((f^[k✝]) x)
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hy
f ((g^[k✝]) x) < (g^[k✝ + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

k✝: β„•

a✝: k✝ < n

hy
f ((g^[k✝]) x) < (g^[k✝ + 1]) x
Ξ±: Type u_1

inst✝: Preorder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

hx: f x < g x

n: β„•

hn: 0 < n

hy
βˆ€ (k : β„•), k < n β†’ f ((g^[k]) x) < (g^[k + 1]) x
Goals accomplished! πŸ™

#align function.commute.iterate_pos_lt_of_map_lt 
Function.Commute.iterate_pos_lt_of_map_lt: βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±}, f x < g x β†’ βˆ€ {n : β„•}, 0 < n β†’ (f^[n]) x < (g^[n]) x
Function.Commute.iterate_pos_lt_of_map_lt

theorem 
iterate_pos_lt_of_map_lt': βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ StrictMono f β†’ Monotone g β†’ βˆ€ {x : Ξ±}, f x < g x β†’ βˆ€ {n : β„•}, 0 < n β†’ (f^[n]) x < (g^[n]) x
iterate_pos_lt_of_map_lt' (
h: Commute f g
h : 
Commute: {Ξ± : Type ?u.6722} β†’ (Ξ± β†’ Ξ±) β†’ (Ξ± β†’ Ξ±) β†’ Prop
Commute 
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g) (
hf: StrictMono f
hf : 
StrictMono: {Ξ± : Type ?u.6733} β†’ {Ξ² : Type ?u.6732} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono 
f: Ξ± β†’ Ξ±
f) (
hg: Monotone g
hg : 
Monotone: {Ξ± : Type ?u.6765} β†’ {Ξ² : Type ?u.6764} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
g: Ξ± β†’ Ξ±
g) {
x: Ξ±
x}
    (
hx: f x < g x
hx : 
f: Ξ± β†’ Ξ±
f 
x: ?m.6793
x < 
g: Ξ± β†’ Ξ±
g 
x: ?m.6793
x) {
n: β„•
n} (
hn: 0 < n
hn : 
0: ?m.6814
0 < 
n: ?m.6809
n) : (
f: Ξ± β†’ Ξ±
f^[
n: ?m.6809
n]) 
x: ?m.6793
x < (
g: Ξ± β†’ Ξ±
g^[
n: ?m.6809
n]) 
x: ?m.6793
x :=
  @
iterate_pos_lt_of_map_lt: βˆ€ {Ξ± : Type ?u.6913} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±}, f x < g x β†’ βˆ€ {n : β„•}, 0 < n β†’ (f^[n]) x < (g^[n]) x
iterate_pos_lt_of_map_lt 
Ξ±: ?m.6708
Ξ±α΅’α΅ˆ _ 
g: Ξ± β†’ Ξ±
g 
f: Ξ± β†’ Ξ±
f 
h: Commute f g
h.
symm: βˆ€ {Ξ± : Type ?u.6922} {f g : Ξ± β†’ Ξ±}, Commute f g β†’ Commute g f
symm 
hg: Monotone g
hg.
dual: βˆ€ {Ξ± : Type ?u.6940} {Ξ² : Type ?u.6939} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual 
hf: StrictMono f
hf.
dual: βˆ€ {Ξ± : Type ?u.6973} {Ξ² : Type ?u.6972} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  StrictMono f β†’ StrictMono (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual 
x: Ξ±
x 
hx: f x < g x
hx 
n: β„•
n 
hn: 0 < n
hn
#align function.commute.iterate_pos_lt_of_map_lt' 
Function.Commute.iterate_pos_lt_of_map_lt': βˆ€ {Ξ± : Type u_1} [inst : Preorder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ StrictMono f β†’ Monotone g β†’ βˆ€ {x : Ξ±}, f x < g x β†’ βˆ€ {n : β„•}, 0 < n β†’ (f^[n]) x < (g^[n]) x
Function.Commute.iterate_pos_lt_of_map_lt'

end Preorder

variable [
LinearOrder: Type ?u.7034 β†’ Type ?u.7034
LinearOrder 
Ξ±: ?m.7047
Ξ±] {
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g : 
Ξ±: ?m.7031
Ξ± β†’ 
Ξ±: ?m.7031
Ξ±}

theorem 
iterate_pos_lt_iff_map_lt: Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±} {n : β„•}, 0 < n β†’ ((f^[n]) x < (g^[n]) x ↔ f x < g x)
iterate_pos_lt_iff_map_lt (
h: Commute f g
h : 
Commute: {Ξ± : Type ?u.7061} β†’ (Ξ± β†’ Ξ±) β†’ (Ξ± β†’ Ξ±) β†’ Prop
Commute 
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g) (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.7072} β†’ {Ξ² : Type ?u.7071} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: Ξ± β†’ Ξ±
f) (
hg: StrictMono g
hg : 
StrictMono: {Ξ± : Type ?u.7122} β†’ {Ξ² : Type ?u.7121} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono 
g: Ξ± β†’ Ξ±
g) {
x: Ξ±
x 
n: ?m.7161
n}
    (
hn: 0 < n
hn : 
0: ?m.7166
0 < 
n: ?m.7161
n) : (
f: Ξ± β†’ Ξ±
f^[
n: ?m.7161
n]) 
x: ?m.7158
x < (
g: Ξ± β†’ Ξ±
g^[
n: ?m.7161
n]) 
x: ?m.7158
x ↔ 
f: Ξ± β†’ Ξ±
f 
x: ?m.7158
x < 
g: Ξ± β†’ Ξ±
g 
x: ?m.7158
x := 
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x < g x

inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x = g x

inr.inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: g x < f x

inr.inr
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x < g x

inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x < g x

inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x = g x

inr.inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: g x < f x

inr.inr
(f^[n]) x < (g^[n]) x ↔ f x < g x
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x = g x

inr.inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: f x = g x

inr.inl
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: g x < f x

inr.inr
(f^[n]) x < (g^[n]) x ↔ f x < g x
Goals accomplished! πŸ™
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: g x < f x

inr.inr
(f^[n]) x < (g^[n]) x ↔ f x < g x
Ξ±: Type u_1

inst✝: LinearOrder α

f, g: Ξ± β†’ Ξ±

h: Commute f g

hf: Monotone f

hg: StrictMono g

x: Ξ±

n: β„•

hn: 0 < n

H: g x < f x

inr.inr
(f^[n]) x < (g^[n]) x ↔ f x < g x
Goals accomplished! πŸ™

#align function.commute.iterate_pos_lt_iff_map_lt 
Function.Commute.iterate_pos_lt_iff_map_lt: βˆ€ {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±} {n : β„•}, 0 < n β†’ ((f^[n]) x < (g^[n]) x ↔ f x < g x)
Function.Commute.iterate_pos_lt_iff_map_lt

theorem 
iterate_pos_lt_iff_map_lt': βˆ€ {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ StrictMono f β†’ Monotone g β†’ βˆ€ {x : Ξ±} {n : β„•}, 0 < n β†’ ((f^[n]) x < (g^[n]) x ↔ f x < g x)
iterate_pos_lt_iff_map_lt' (
h: Commute f g
h : 
Commute: {Ξ± : Type ?u.7913} β†’ (Ξ± β†’ Ξ±) β†’ (Ξ± β†’ Ξ±) β†’ Prop
Commute 
f: Ξ± β†’ Ξ±
f 
g: Ξ± β†’ Ξ±
g) (
hf: StrictMono f
hf : 
StrictMono: {Ξ± : Type ?u.7924} β†’ {Ξ² : Type ?u.7923} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
StrictMono 
f: Ξ± β†’ Ξ±
f) (
hg: Monotone g
hg : 
Monotone: {Ξ± : Type ?u.7974} β†’ {Ξ² : Type ?u.7973} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
g: Ξ± β†’ Ξ±
g) {
x: ?m.8010
x 
n: ?m.8013
n}
    (
hn: 0 < n
hn : 
0: ?m.8018
0 < 
n: ?m.8013
n) : (
f: Ξ± β†’ Ξ±
f^[
n: ?m.8013
n]) 
x: ?m.8010
x < (
g: Ξ± β†’ Ξ±
g^[
n: ?m.8013
n]) 
x: ?m.8010
x ↔ 
f: Ξ± β†’ Ξ±
f 
x: ?m.8010
x < 
g: Ξ± β†’ Ξ±
g 
x: ?m.8010
x :=
  @
iterate_pos_lt_iff_map_lt: βˆ€ {Ξ± : Type ?u.8124} [inst : LinearOrder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ Monotone f β†’ StrictMono g β†’ βˆ€ {x : Ξ±} {n : β„•}, 0 < n β†’ ((f^[n]) x < (g^[n]) x ↔ f x < g x)
iterate_pos_lt_iff_map_lt 
Ξ±: ?m.7899
Ξ±α΅’α΅ˆ _ 
_: Ξ±α΅’α΅ˆ β†’ Ξ±α΅’α΅ˆ
_ 
_: Ξ±α΅’α΅ˆ β†’ Ξ±α΅’α΅ˆ
_ 
h: Commute f g
h.
symm: βˆ€ {Ξ± : Type ?u.8129} {f g : Ξ± β†’ Ξ±}, Commute f g β†’ Commute g f
symm 
hg: Monotone g
hg.
dual: βˆ€ {Ξ± : Type ?u.8149} {Ξ² : Type ?u.8148} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  Monotone f β†’ Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual 
hf: StrictMono f
hf.
dual: βˆ€ {Ξ± : Type ?u.8223} {Ξ² : Type ?u.8222} [inst : Preorder Ξ±] [inst_1 : Preorder Ξ²] {f : Ξ± β†’ Ξ²},
  StrictMono f β†’ StrictMono (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual 
x: Ξ±
x 
n: β„•
n 
hn: 0 < n
hn
#align function.commute.iterate_pos_lt_iff_map_lt' 
Function.Commute.iterate_pos_lt_iff_map_lt': βˆ€ {Ξ± : Type u_1} [inst : LinearOrder Ξ±] {f g : Ξ± β†’ Ξ±},
  Commute f g β†’ StrictMono f β†’ Monotone g β†’ βˆ€ {x : Ξ±} {n : β„•}, 0 < n β†’ ((f^[n]) x < (g^[n]) x ↔ f x < g x)
Function.Commute.iterate_pos_lt_iff_map_lt'

theorem 
iterate_pos_le_iff_map_le: