Archimedean

📁 Source: Mathlib/Order/SuccPred/Archimedean.lean

Statistics

Metric	Count
Definitions IsPredArchimedean, linearOrder, IsSuccArchimedean, linearOrder	4
Theorems exists_isGreatest_of_nonempty, exists_isLeast_of_nonempty, exists_pred_iterate_of_le, of_orderIso, exists_succ_iterate_of_le, of_orderIso, exists_pred_iterate, exists_succ_iterate, rec, rec_iff, rec_linear, rec_top, isPredArchimedean, isSuccArchimedean, not_bddBelow_range_of_isPredArchimedean, not_bddBelow_range_of_isSuccArchimedean, not_bddAbove_range_of_isSuccArchimedean, not_bddBelow_range_of_isPredArchimedean, rec, rec_bot, rec_iff, rec_linear, forall_ne_bot_iff, toIsSuccArchimedean, toIsPredArchimedean, antitoneOn_of_le_pred, antitoneOn_of_succ_le, antitone_of_le_pred, antitone_of_succ_le, exists_pred_iterate_iff_le, exists_pred_iterate_or, exists_succ_iterate_iff_le, exists_succ_iterate_or, instIsPredArchimedeanOrderDual, instIsSuccArchimedeanOrderDual, le_total_of_codirected, le_total_of_directed, lt_or_le_of_codirected, lt_or_le_of_directed, monotoneOn_of_le_succ, monotoneOn_of_pred_le, monotone_of_le_succ, monotone_of_pred_le, pred_max, pred_min, strictAntiOn_of_lt_pred, strictAntiOn_of_succ_lt, strictAnti_of_lt_pred, strictAnti_of_succ_lt, strictMonoOn_of_lt_succ, strictMonoOn_of_pred_lt, strictMono_of_lt_succ, strictMono_of_pred_lt, succ_max, succ_min	55
Total	59

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isGreatest_of_nonempty 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	IsGreatest	—	instIsEmptyFalse mem_upperBounds

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isLeast_of_nonempty 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Nonempty	IsLeast	—	BddAbove.exists_isGreatest_of_nonempty instIsSuccArchimedeanOrderDual dual

IsPredArchimedean

Definitions

Name	Category	Theorems
linearOrder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pred_iterate_of_le 📖	mathematical	Preorder.toLE	Nat.iterate Order.pred	—	—
of_orderIso 📖	mathematical	—	IsPredArchimedean PartialOrder.toPreorder	—	OrderIso.apply_eq_iff_eq EquivLike.apply_inv_apply Function.iterate_succ' OrderIso.map_pred exists_pred_iterate_of_le map_inv_le_map_inv_iff OrderIso.instOrderIsoClass

IsSuccArchimedean

Definitions

Name	Category	Theorems
linearOrder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_succ_iterate_of_le 📖	mathematical	Preorder.toLE	Nat.iterate Order.succ	—	—
of_orderIso 📖	mathematical	—	IsSuccArchimedean PartialOrder.toPreorder	—	OrderIso.apply_eq_iff_eq EquivLike.apply_inv_apply Function.iterate_succ' OrderIso.map_succ exists_succ_iterate_of_le map_inv_le_map_inv_iff OrderIso.instOrderIsoClass

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pred_iterate 📖	mathematical	Preorder.toLE	Nat.iterate Order.pred	—	IsPredArchimedean.exists_pred_iterate_of_le
exists_succ_iterate 📖	mathematical	Preorder.toLE	Nat.iterate Order.succ	—	IsSuccArchimedean.exists_succ_iterate_of_le

Pred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rec 📖	—	le_rfl Order.pred LE.le.trans Order.pred_le Preorder.toLE	—	—	le_rfl LE.le.trans Order.pred_le instIsSuccArchimedeanOrderDual
rec_iff 📖	—	Order.pred Preorder.toLE	—	—	Succ.rec_iff instIsSuccArchimedeanOrderDual
rec_linear 📖	—	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_total rec_iff
rec_top 📖	—	Top.top OrderTop.toTop Preorder.toLE Order.pred	—	—	le_top

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPredArchimedean 📖	mathematical	—	IsPredArchimedean Set.Elem Subtype.preorder PartialOrder.toPreorder Set Set.instMembership predOrder	—	LE.le.exists_pred_iterate Order.pred_iterate_le Function.iterate_fixed IsMin.eq_of_le
isSuccArchimedean 📖	mathematical	—	IsSuccArchimedean Set.Elem Subtype.preorder PartialOrder.toPreorder Set Set.instMembership succOrder	—	instIsSuccArchimedeanOrderDual Set.dual_ordConnected isPredArchimedean instIsPredArchimedeanOrderDual

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_bddBelow_range_of_isPredArchimedean 📖	mathematical	StrictAnti	BddBelow Preorder.toLE Set.range	—	StrictMono.not_bddAbove_range_of_isSuccArchimedean instIsSuccArchimedeanOrderDual dual_right
not_bddBelow_range_of_isSuccArchimedean 📖	mathematical	StrictAnti	BddAbove Preorder.toLE Set.range	—	StrictMono.not_bddBelow_range_of_isPredArchimedean instIsPredArchimedeanOrderDual dual_right

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_bddAbove_range_of_isSuccArchimedean 📖	mathematical	StrictMono	BddAbove Preorder.toLE Set.range	—	Set.mem_range_self NoMaxOrder.exists_gt LE.le.trans_lt Order.succ_le_of_lt LT.lt.not_ge
not_bddBelow_range_of_isPredArchimedean 📖	mathematical	StrictMono	BddBelow Preorder.toLE Set.range	—	not_bddAbove_range_of_isSuccArchimedean OrderDual.instNonempty OrderDual.noMaxOrder instIsSuccArchimedeanOrderDual dual

Succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rec 📖	—	le_rfl Order.succ LE.le.trans Order.le_succ Preorder.toLE	—	—	le_rfl LE.le.trans Order.le_succ LE.le.exists_succ_iterate Function.iterate_succ_apply' Function.id_le_iterate_of_id_le
rec_bot 📖	—	Bot.bot OrderBot.toBot Preorder.toLE Order.succ	—	—	bot_le
rec_iff 📖	—	Order.succ Preorder.toLE	—	—	LE.le.exists_succ_iterate
rec_linear 📖	—	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	le_total rec_iff

SuccOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_ne_bot_iff 📖	mathematical	—	succ PartialOrder.toPreorder	—	Order.succ_ne_bot IsSuccArchimedean.exists_succ_iterate_of_le bot_le Mathlib.Tactic.Contrapose.contrapose₄ Function.iterate_succ'

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsSuccArchimedean 📖	mathematical	—	IsSuccArchimedean PartialOrder.toPreorder	—	WellFoundedLT.toIsPredArchimedean instWellFoundedLTOrderDualOfWellFoundedGT IsPredArchimedean.exists_pred_iterate_of_le

WellFoundedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsPredArchimedean 📖	mathematical	—	IsPredArchimedean PartialOrder.toPreorder	—	IsWellFounded.wf eq_or_lt_of_le Order.pred_le IsMin.not_lt Order.min_of_le_pred Eq.ge Order.le_pred_of_lt Function.iterate_add_apply Function.iterate_one

(root)

Definitions

Name	Category	Theorems
IsPredArchimedean 📖	CompData	12 math math: LinearOrder.isSuccArchimedean_iff_isPredArchimedean, WellFoundedLT.toIsPredArchimedean, LinearLocallyFiniteOrder.instIsPredArchimedeanOfLocallyFiniteOrder, instIsPredArchimedeanOrderDual, Int.instIsPredArchimedean, instIsPredArchimedeanMultiplicative, RootedTree.isPredArchimedean, instIsPredArchimedeanAdditive, IsPredArchimedean.of_orderIso, Set.OrdConnected.isPredArchimedean, LinearOrder.isPredArchimedean_of_isSuccArchimedean, Nat.instIsPredArchimedean
IsSuccArchimedean 📖	CompData	11 math math: LinearOrder.isSuccArchimedean_iff_isPredArchimedean, Int.instIsSuccArchimedean, instIsSuccArchimedeanOrderDual, instIsSuccArchimedeanAdditive, Nat.instIsSuccArchimedean, Set.OrdConnected.isSuccArchimedean, LinearLocallyFiniteOrder.instIsSuccArchimedeanOfLocallyFiniteOrder, LinearOrder.isSuccArchimedean_of_isPredArchimedean, IsSuccArchimedean.of_orderIso, WellFoundedGT.toIsSuccArchimedean, instIsSuccArchimedeanMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_of_le_pred 📖	mathematical	Preorder.toLE Order.pred PartialOrder.toPreorder	AntitoneOn	—	monotoneOn_of_pred_le
antitoneOn_of_succ_le 📖	mathematical	Preorder.toLE Order.succ PartialOrder.toPreorder	AntitoneOn	—	monotoneOn_of_le_succ
antitone_of_le_pred 📖	mathematical	Preorder.toLE Order.pred PartialOrder.toPreorder	Antitone	—	antitoneOn_of_le_pred Set.ordConnected_univ
antitone_of_succ_le 📖	mathematical	Preorder.toLE Order.succ PartialOrder.toPreorder	Antitone	—	antitoneOn_of_succ_le Set.ordConnected_univ
exists_pred_iterate_iff_le 📖	mathematical	—	Nat.iterate Order.pred Preorder.toLE	—	exists_succ_iterate_iff_le instIsSuccArchimedeanOrderDual
exists_pred_iterate_or 📖	mathematical	—	Nat.iterate Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsPredArchimedean.exists_pred_iterate_of_le le_total
exists_succ_iterate_iff_le 📖	mathematical	—	Nat.iterate Order.succ Preorder.toLE	—	Function.id_le_iterate_of_id_le Order.le_succ IsSuccArchimedean.exists_succ_iterate_of_le
exists_succ_iterate_or 📖	mathematical	—	Nat.iterate Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	IsSuccArchimedean.exists_succ_iterate_of_le le_total
instIsPredArchimedeanOrderDual 📖	mathematical	—	IsPredArchimedean OrderDual OrderDual.instPreorder instPredOrderOrderDualOfSuccOrder	—	IsSuccArchimedean.exists_succ_iterate_of_le LE.le.ofDual
instIsSuccArchimedeanOrderDual 📖	mathematical	—	IsSuccArchimedean OrderDual OrderDual.instPreorder instSuccOrderOrderDualOfPredOrder	—	IsPredArchimedean.exists_pred_iterate_of_le LE.le.ofDual
le_total_of_codirected 📖	—	Preorder.toLE	—	—	LE.le.exists_succ_iterate Function.iterate_add Order.le_succ_iterate
le_total_of_directed 📖	—	Preorder.toLE	—	—	le_total_of_codirected instIsSuccArchimedeanOrderDual
lt_or_le_of_codirected 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	le_total_of_codirected lt_of_le_of_ne ne_of_not_le
lt_or_le_of_directed 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	le_total_of_directed lt_of_le_of_ne ne_of_not_le
monotoneOn_of_le_succ 📖	mathematical	Preorder.toLE Order.succ PartialOrder.toPreorder	MonotoneOn	—	IsSuccArchimedean.exists_succ_iterate_of_le Function.iterate_succ_apply' Set.OrdConnected.out' Order.le_succ_iterate Order.le_succ Order.succ_eq_iff_isMax LE.le.trans
monotoneOn_of_pred_le 📖	mathematical	Preorder.toLE Order.pred PartialOrder.toPreorder	MonotoneOn	—	IsPredArchimedean.exists_pred_iterate_of_le Function.iterate_succ_apply' Set.OrdConnected.out' Order.pred_le Order.pred_iterate_le Order.pred_eq_iff_isMin LE.le.trans'
monotone_of_le_succ 📖	mathematical	Preorder.toLE Order.succ PartialOrder.toPreorder	Monotone	—	monotoneOn_of_le_succ Set.ordConnected_univ
monotone_of_pred_le 📖	mathematical	Preorder.toLE Order.pred PartialOrder.toPreorder	Monotone	—	monotoneOn_of_pred_le Set.ordConnected_univ
pred_max 📖	mathematical	—	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max Order.pred_mono
pred_min 📖	mathematical	—	Order.pred PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	Monotone.map_min Order.pred_mono
strictAntiOn_of_lt_pred 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictAntiOn	—	strictMonoOn_of_pred_lt
strictAntiOn_of_succ_lt 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictAntiOn	—	strictMonoOn_of_lt_succ
strictAnti_of_lt_pred 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictAnti	—	strictAntiOn_of_lt_pred Set.ordConnected_univ
strictAnti_of_succ_lt 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictAnti	—	strictAntiOn_of_succ_lt Set.ordConnected_univ
strictMonoOn_of_lt_succ 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictMonoOn	—	IsSuccArchimedean.exists_succ_iterate_of_le LT.lt.le Function.iterate_one not_isMax_of_lt Function.iterate_succ_apply' Set.OrdConnected.out' Order.le_succ_iterate Order.le_succ Order.succ_eq_iff_isMax LT.lt.trans
strictMonoOn_of_pred_lt 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictMonoOn	—	IsPredArchimedean.exists_pred_iterate_of_le LT.lt.le Function.iterate_one not_isMin_of_lt Function.iterate_succ_apply' Set.OrdConnected.out' Order.pred_le Order.pred_iterate_le Order.pred_eq_iff_isMin LT.lt.trans'
strictMono_of_lt_succ 📖	mathematical	Preorder.toLT Order.succ PartialOrder.toPreorder	StrictMono	—	strictMonoOn_of_lt_succ Set.ordConnected_univ
strictMono_of_pred_lt 📖	mathematical	Preorder.toLT Order.pred PartialOrder.toPreorder	StrictMono	—	strictMonoOn_of_pred_lt Set.ordConnected_univ
succ_max 📖	mathematical	—	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max Order.succ_mono
succ_min 📖	mathematical	—	Order.succ PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	Monotone.map_min Order.succ_mono

---

← Back to Index