MonotoneConvergence

📁 Source: Mathlib/Topology/Order/MonotoneConvergence.lean

Statistics

Metric	Count
Definitions InfConvergenceClass, SupConvergenceClass	2
Theorems ge_of_tendsto, le_of_tendsto, tendsto_coe_atBot_isGLB, infConvergenceClass, supConvergenceClass, ge_of_tendsto, le_of_tendsto, infConvergenceClass, supConvergenceClass, infConvergenceClass, infConvergenceClass', supConvergenceClass, supConvergenceClass', supConvergenceClass, tendsto_coe_atTop_isLUB, iInf_eq_iInf_subseq_of_antitone, iInf_eq_iInf_subseq_of_monotone, iInf_eq_of_tendsto, iSup_eq_iSup_subseq_of_antitone, iSup_eq_iSup_subseq_of_monotone, iSup_eq_of_tendsto, instInfConvergenceClassProd, isGLB_of_tendsto_atBot, isGLB_of_tendsto_atTop, isLUB_of_tendsto_atBot, isLUB_of_tendsto_atTop, tendsto_atBot_ciInf, tendsto_atBot_ciSup, tendsto_atBot_iInf, tendsto_atBot_iSup, tendsto_atBot_isGLB, tendsto_atBot_isLUB, tendsto_atBot_of_antitone, tendsto_atBot_of_monotone, tendsto_atTop_ciInf, tendsto_atTop_ciSup, tendsto_atTop_iInf, tendsto_atTop_iSup, tendsto_atTop_isGLB, tendsto_atTop_isLUB, tendsto_atTop_of_antitone, tendsto_atTop_of_monotone, tendsto_iff_tendsto_subseq_of_antitone, tendsto_iff_tendsto_subseq_of_monotone, tendsto_of_antitone, tendsto_of_monotone	46
Total	48

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ge_of_tendsto 📖	mathematical	Antitone Filter.Tendsto Filter.atBot nhds	Preorder.toLE	—	Monotone.le_of_tendsto instOrderClosedTopologyOrderDual dual_right
le_of_tendsto 📖	mathematical	Antitone Filter.Tendsto Filter.atTop nhds	Preorder.toLE	—	Monotone.ge_of_tendsto instOrderClosedTopologyOrderDual dual_right

InfConvergenceClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_coe_atBot_isGLB 📖	mathematical	IsGLB Preorder.toLE	Filter.Tendsto Set Set.instMembership Filter.atBot Subtype.preorder nhds	—	—

LinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infConvergenceClass 📖	mathematical	—	InfConvergenceClass PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	OrderDual.infConvergenceClass supConvergenceClass instOrderTopologyOrderDual
supConvergenceClass 📖	mathematical	—	SupConvergenceClass PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	tendsto_order IsLUB.exists_between CanLift.prf Subtype.canLift Filter.Eventually.mono Filter.eventually_ge_atTop LT.lt.trans_le Filter.Eventually.of_forall LE.le.trans_lt

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ge_of_tendsto 📖	mathematical	Monotone Filter.Tendsto Filter.atTop nhds	Preorder.toLE	—	ge_of_tendsto instClosedIciTopology Filter.atTop_neBot Filter.Eventually.mono Filter.eventually_ge_atTop
le_of_tendsto 📖	mathematical	Monotone Filter.Tendsto Filter.atBot nhds	Preorder.toLE	—	ge_of_tendsto instOrderClosedTopologyOrderDual OrderDual.isDirected_le dual

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infConvergenceClass 📖	mathematical	—	InfConvergenceClass OrderDual instPreorder instTopologicalSpace	—	SupConvergenceClass.tendsto_coe_atTop_isLUB
supConvergenceClass 📖	mathematical	—	SupConvergenceClass OrderDual instPreorder instTopologicalSpace	—	InfConvergenceClass.tendsto_coe_atBot_isGLB

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infConvergenceClass 📖	mathematical	InfConvergenceClass	preorder topologicalSpace	—	OrderDual.infConvergenceClass supConvergenceClass OrderDual.supConvergenceClass
infConvergenceClass' 📖	mathematical	—	InfConvergenceClass preorder topologicalSpace	—	infConvergenceClass
supConvergenceClass 📖	mathematical	SupConvergenceClass	preorder topologicalSpace	—	tendsto_pi_nhds tendsto_atTop_isLUB Monotone.restrict Function.monotone_eval
supConvergenceClass' 📖	mathematical	—	SupConvergenceClass preorder topologicalSpace	—	supConvergenceClass

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
supConvergenceClass 📖	mathematical	—	SupConvergenceClass instPreorder instTopologicalSpaceProd	—	tendsto_atTop_isLUB Monotone.restrict monotone_fst Set.range_restrict isLUB_prod monotone_snd Filter.Tendsto.prodMk_nhds

SupConvergenceClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_coe_atTop_isLUB 📖	mathematical	IsLUB Preorder.toLE	Filter.Tendsto Set Set.instMembership Filter.atTop Subtype.preorder nhds	—	—

(root)

Definitions

Name	Category	Theorems
InfConvergenceClass 📖	CompData	4 math math: instInfConvergenceClassProd, LinearOrder.infConvergenceClass, OrderDual.infConvergenceClass, Pi.infConvergenceClass'
SupConvergenceClass 📖	CompData	4 math math: LinearOrder.supConvergenceClass, OrderDual.supConvergenceClass, Pi.supConvergenceClass', Prod.supConvergenceClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_eq_iInf_subseq_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	iSup_eq_iSup_subseq_of_antitone Antitone.dual
iInf_eq_iInf_subseq_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Filter.Tendsto Filter.atBot	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	iSup_eq_iSup_subseq_of_monotone Monotone.dual
iInf_eq_of_tendsto 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeSup.toPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Filter.Tendsto Filter.atTop nhds	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	tendsto_nhds_unique OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder tendsto_atTop_iInf LinearOrder.infConvergenceClass
iSup_eq_iSup_subseq_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Filter.Tendsto Filter.atBot	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	le_antisymm iSup_mono' Filter.Eventually.exists Filter.Tendsto.eventually Filter.eventually_le_atBot le_rfl
iSup_eq_iSup_subseq_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	le_antisymm iSup_mono' Filter.Eventually.exists Filter.Tendsto.eventually Filter.eventually_ge_atTop le_rfl
iSup_eq_of_tendsto 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeSup.toPartialOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Filter.Tendsto Filter.atTop nhds	iSup ConditionallyCompletePartialOrderSup.toSupSet	—	tendsto_nhds_unique OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder tendsto_atTop_iSup LinearOrder.supConvergenceClass
instInfConvergenceClassProd 📖	mathematical	—	InfConvergenceClass Prod.instPreorder instTopologicalSpaceProd	—	OrderDual.infConvergenceClass Prod.supConvergenceClass OrderDual.supConvergenceClass
isGLB_of_tendsto_atBot 📖	mathematical	Monotone Filter.Tendsto Filter.atBot nhds	IsGLB Preorder.toLE Set.range	—	isLUB_of_tendsto_atTop instOrderClosedTopologyOrderDual OrderDual.isDirected_le OrderDual.instNonempty Monotone.dual
isGLB_of_tendsto_atTop 📖	mathematical	Antitone Filter.Tendsto Filter.atTop nhds	IsGLB Preorder.toLE Set.range	—	isGLB_of_tendsto_atBot OrderDual.isDirected_ge OrderDual.instNonempty Antitone.dual_left
isLUB_of_tendsto_atBot 📖	mathematical	Antitone Filter.Tendsto Filter.atBot nhds	IsLUB Preorder.toLE Set.range	—	isLUB_of_tendsto_atTop OrderDual.isDirected_le OrderDual.instNonempty Antitone.dual_left
isLUB_of_tendsto_atTop 📖	mathematical	Monotone Filter.Tendsto Filter.atTop nhds	IsLUB Preorder.toLE Set.range	—	Monotone.ge_of_tendsto le_of_tendsto' instClosedIicTopology Filter.atTop_neBot Set.mem_range_self
tendsto_atBot_ciInf 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddBelow Preorder.toLE Set.range	Filter.Tendsto Filter.atBot nhds iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	tendsto_atTop_ciSup OrderDual.supConvergenceClass Monotone.dual BddBelow.dual
tendsto_atBot_ciSup 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddAbove Preorder.toLE Set.range	Filter.Tendsto Filter.atBot nhds iSup ConditionallyCompletePartialOrderSup.toSupSet	—	tendsto_atTop_ciSup Antitone.dual BddAbove.dual
tendsto_atBot_iInf 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	Filter.Tendsto Filter.atBot nhds iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	tendsto_atBot_ciInf OrderBot.bddBelow
tendsto_atBot_iSup 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	Filter.Tendsto Filter.atBot nhds iSup ConditionallyCompletePartialOrderSup.toSupSet	—	tendsto_atBot_ciSup OrderTop.bddAbove
tendsto_atBot_isGLB 📖	mathematical	Monotone IsGLB Preorder.toLE Set.range	Filter.Tendsto Filter.atBot nhds	—	tendsto_atTop_isLUB OrderDual.supConvergenceClass Monotone.dual IsGLB.dual
tendsto_atBot_isLUB 📖	mathematical	Antitone IsLUB Preorder.toLE Set.range	Filter.Tendsto Filter.atBot nhds	—	tendsto_atTop_isLUB Antitone.dual_left
tendsto_atBot_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atBot Filter.atTop nhds	—	tendsto_atTop_of_antitone instOrderTopologyOrderDual Antitone.dual
tendsto_atBot_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atBot nhds	—	tendsto_atTop_of_monotone instOrderTopologyOrderDual Monotone.dual
tendsto_atTop_ciInf 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddBelow Preorder.toLE Set.range	Filter.Tendsto Filter.atTop nhds iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	tendsto_atBot_ciSup OrderDual.supConvergenceClass Antitone.dual BddBelow.dual
tendsto_atTop_ciSup 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddAbove Preorder.toLE Set.range	Filter.Tendsto Filter.atTop nhds iSup ConditionallyCompletePartialOrderSup.toSupSet	—	isEmpty_or_nonempty Filter.tendsto_of_isEmpty tendsto_atTop_isLUB isLUB_ciSup
tendsto_atTop_iInf 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop nhds iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	tendsto_atTop_ciInf OrderBot.bddBelow
tendsto_atTop_iSup 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop nhds iSup ConditionallyCompletePartialOrderSup.toSupSet	—	tendsto_atTop_ciSup OrderTop.bddAbove
tendsto_atTop_isGLB 📖	mathematical	Antitone IsGLB Preorder.toLE Set.range	Filter.Tendsto Filter.atTop nhds	—	tendsto_atBot_isLUB OrderDual.supConvergenceClass Antitone.dual IsGLB.dual
tendsto_atTop_isLUB 📖	mathematical	Monotone IsLUB Preorder.toLE Set.range	Filter.Tendsto Filter.atTop nhds	—	Monotone.tendsto_atTop_atTop Monotone.rangeFactorization Eq.ge Filter.Tendsto.comp SupConvergenceClass.tendsto_coe_atTop_isLUB
tendsto_atTop_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop Filter.atBot nhds	—	tendsto_atTop_of_monotone instOrderTopologyOrderDual
tendsto_atTop_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop nhds	—	tendsto_atTop_ciSup LinearOrder.supConvergenceClass Filter.tendsto_atTop_atTop_of_monotone'
tendsto_iff_tendsto_subseq_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop SemilatticeSup.toPartialOrder	nhds	—	tendsto_iff_tendsto_subseq_of_monotone instOrderTopologyOrderDual OrderDual.noMaxOrder
tendsto_iff_tendsto_subseq_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.Tendsto Filter.atTop SemilatticeSup.toPartialOrder	nhds	—	Filter.Tendsto.comp tendsto_atTop_of_monotone not_tendsto_atTop_of_tendsto_nhds instNoTopOrderOfNoMaxOrder instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder tendsto_nhds_unique OrderClosedTopology.to_t2Space
tendsto_of_antitone 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop Filter.atBot nhds	—	tendsto_atTop_of_antitone
tendsto_of_monotone 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Tendsto Filter.atTop nhds	—	tendsto_atTop_of_monotone

---

← Back to Index