Iterate

📁 Source: Mathlib/Order/Iterate.lean

Statistics

Metric	Count
Definitions	0
Theorems iterate_le_of_map_le, iterate_pos_eq_iff_map_eq, iterate_pos_le_iff_map_le, iterate_pos_le_iff_map_le', iterate_pos_lt_iff_map_lt, iterate_pos_lt_iff_map_lt', iterate_pos_lt_of_map_lt, iterate_pos_lt_of_map_lt', antitone_iterate_of_le_id, id_le_iterate_of_id_le, iterate_le_id_of_le_id, monotone_iterate_of_id_le, antitone_iterate_of_map_le, iterate_comp_le_of_le, iterate_le_of_le, le_iterate_comp_of_le, le_iterate_of_le, monotone_iterate_of_le_map, seq_le_seq, seq_lt_seq_of_le_of_lt, seq_lt_seq_of_lt_of_le, seq_pos_lt_seq_of_le_of_lt, seq_pos_lt_seq_of_lt_of_le, strictAnti_iterate_of_map_lt, strictMono_iterate_of_lt_map	25
Total	25

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_iterate_of_le_id 📖	mathematical	Pi.hasLe Preorder.toLE	Antitone Nat.instPreorder Pi.preorder Nat.iterate	—	monotone_iterate_of_id_le
id_le_iterate_of_id_le 📖	mathematical	Pi.hasLe Preorder.toLE	Nat.iterate	—	iterate_id Monotone.iterate_le_of_le monotone_id
iterate_le_id_of_le_id 📖	mathematical	Pi.hasLe Preorder.toLE	Nat.iterate	—	iterate_id Monotone.le_iterate_of_le monotone_id
monotone_iterate_of_id_le 📖	mathematical	Pi.hasLe Preorder.toLE	Monotone Nat.instPreorder Pi.preorder Nat.iterate	—	monotone_nat_of_le_succ iterate_succ_apply'

Function.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iterate_le_of_map_le 📖	mathematical	Function.Commute Monotone Preorder.toLE	Nat.iterate	—	Monotone.seq_le_seq le_refl Function.iterate_succ_apply' iterate_right Monotone.iterate
iterate_pos_eq_iff_map_eq 📖	mathematical	Function.Commute Monotone PartialOrder.toPreorder LinearOrder.toPartialOrder StrictMono	Nat.iterate	—	iterate_pos_le_iff_map_le iterate_pos_le_iff_map_le' symm
iterate_pos_le_iff_map_le 📖	mathematical	Function.Commute Monotone PartialOrder.toPreorder LinearOrder.toPartialOrder StrictMono	Preorder.toLE Nat.iterate	—	iterate_pos_lt_iff_map_lt' symm
iterate_pos_le_iff_map_le' 📖	mathematical	Function.Commute StrictMono PartialOrder.toPreorder LinearOrder.toPartialOrder Monotone	Preorder.toLE Nat.iterate	—	iterate_pos_lt_iff_map_lt symm
iterate_pos_lt_iff_map_lt 📖	mathematical	Function.Commute Monotone PartialOrder.toPreorder LinearOrder.toPartialOrder StrictMono	Preorder.toLT Nat.iterate	—	lt_trichotomy iterate_eq_of_map_eq lt_asymm iterate_pos_lt_of_map_lt' symm
iterate_pos_lt_iff_map_lt' 📖	mathematical	Function.Commute StrictMono PartialOrder.toPreorder LinearOrder.toPartialOrder Monotone	Preorder.toLT Nat.iterate	—	iterate_pos_lt_iff_map_lt symm Monotone.dual StrictMono.dual
iterate_pos_lt_of_map_lt 📖	mathematical	Function.Commute Monotone StrictMono Preorder.toLT	Nat.iterate	—	Monotone.seq_pos_lt_seq_of_le_of_lt le_refl Function.iterate_succ_apply' iterate_right StrictMono.iterate
iterate_pos_lt_of_map_lt' 📖	mathematical	Function.Commute StrictMono Monotone Preorder.toLT	Nat.iterate	—	iterate_pos_lt_of_map_lt symm Monotone.dual StrictMono.dual

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_iterate_of_map_le 📖	mathematical	Monotone Preorder.toLE	Antitone Nat.instPreorder Nat.iterate	—	monotone_iterate_of_le_map dual
iterate_comp_le_of_le 📖	mathematical	Monotone Pi.hasLe Preorder.toLE	Nat.iterate	—	seq_le_seq le_refl Function.iterate_succ'
iterate_le_of_le 📖	mathematical	Monotone Pi.hasLe Preorder.toLE	Nat.iterate	—	iterate_comp_le_of_le
le_iterate_comp_of_le 📖	mathematical	Monotone Pi.hasLe Preorder.toLE	Nat.iterate	—	seq_le_seq Function.iterate_succ'
le_iterate_of_le 📖	mathematical	Monotone Pi.hasLe Preorder.toLE	Nat.iterate	—	le_iterate_comp_of_le
monotone_iterate_of_le_map 📖	mathematical	Monotone Preorder.toLE	Nat.instPreorder Nat.iterate	—	monotone_nat_of_le_succ Function.iterate_succ_apply iterate
seq_le_seq 📖	—	Monotone Preorder.toLE	—	—	LE.le.trans LT.lt.trans
seq_lt_seq_of_le_of_lt 📖	—	Monotone Preorder.toLT Preorder.toLE	—	—	seq_lt_seq_of_lt_of_le dual
seq_lt_seq_of_lt_of_le 📖	—	Monotone Preorder.toLT Preorder.toLE	—	—	seq_pos_lt_seq_of_lt_of_le LT.lt.le
seq_pos_lt_seq_of_le_of_lt 📖	—	Monotone Preorder.toLE Preorder.toLT	—	—	seq_pos_lt_seq_of_lt_of_le dual
seq_pos_lt_seq_of_lt_of_le 📖	—	Monotone Preorder.toLE Preorder.toLT	—	—	LT.lt.false LT.lt.le LT.lt.trans LT.lt.trans_le LE.le.trans

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictAnti_iterate_of_map_lt 📖	mathematical	StrictMono Preorder.toLT	StrictAnti Nat.instPreorder Nat.iterate	—	strictMono_iterate_of_lt_map dual
strictMono_iterate_of_lt_map 📖	mathematical	StrictMono Preorder.toLT	Nat.instPreorder Nat.iterate	—	strictMono_nat_of_lt_succ Function.iterate_succ_apply iterate

---

← Back to Index