Documentation Verification Report

MonotoneContinuity

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

Statistics

Metric	Count
Definitions `toHomeomorph`	1
Theorems `continuous_of_denseRange`, `continuous_of_surjective`, `coe_toHomeomorph`, `coe_toHomeomorph_symm`, `continuous`, `instHomeomorphClass`, `continuousAt_of_closure_image_mem_nhds`, `continuousAt_of_exists_between`, `continuousAt_of_image_mem_nhds`, `continuousWithinAt_left_of_closure_image_mem_nhdsWithin`, `continuousWithinAt_left_of_exists_between`, `continuousWithinAt_left_of_image_mem_nhdsWithin`, `continuousWithinAt_left_of_surjOn`, `continuousWithinAt_right_of_closure_image_mem_nhdsWithin`, `continuousWithinAt_right_of_exists_between`, `continuousWithinAt_right_of_image_mem_nhdsWithin`, `continuousWithinAt_right_of_surjOn`, `continuousAt_of_monotoneOn_of_closure_image_mem_nhds`, `continuousAt_of_monotoneOn_of_exists_between`, `continuousAt_of_monotoneOn_of_image_mem_nhds`, `continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin`, `continuousWithinAt_left_of_monotoneOn_of_exists_between`, `continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin`, `continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin`, `continuousWithinAt_right_of_monotoneOn_of_exists_between`, `continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin`	26
Total	27

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_denseRange` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DenseRange`	`Continuous`	—	`continuous_iff_continuousAt` `continuousAt_of_monotoneOn_of_closure_image_mem_nhds` `Filter.univ_mem` `Set.image_univ` `Dense.closure_eq`
`continuous_of_surjective` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Continuous`	—	`continuous_of_denseRange` `Function.Surjective.denseRange`

OrderIso

Definitions

Name	Category	Theorems
`toHomeomorph` 📖	CompOp	2 math math: `coe_toHomeomorph`, `coe_toHomeomorph_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toHomeomorph` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toHomeomorph` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso`	—	—
`coe_toHomeomorph_symm` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `toHomeomorph` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `symm`	—	—
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso`	—	`OrderTopology.topology_eq_generate_intervals` `continuous_generateFrom_iff` `preimage_Ioi` `isOpen_lt'` `preimage_Iio` `isOpen_gt'`
`instHomeomorphClass` 📖	mathematical	—	`HomeomorphClass` `OrderIso` `Preorder.toLE` `instEquivLike`	—	`continuous`

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_of_closure_image_mem_nhds` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `closure` `Set.image`	`ContinuousAt`	—	`continuousAt_iff_continuous_left_right` `continuousWithinAt_left_of_closure_image_mem_nhdsWithin` `mem_nhdsWithin_of_mem_nhds` `continuousWithinAt_right_of_closure_image_mem_nhdsWithin`
`continuousAt_of_exists_between` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `Set.Ico` `Set.Ioc`	`ContinuousAt`	—	`continuousAt_iff_continuous_left_right` `continuousWithinAt_left_of_exists_between` `mem_nhdsWithin_of_mem_nhds` `continuousWithinAt_right_of_exists_between`
`continuousAt_of_image_mem_nhds` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `Set.image`	`ContinuousAt`	—	`continuousAt_of_closure_image_mem_nhds` `Filter.mem_of_superset` `subset_closure`
`continuousWithinAt_left_of_closure_image_mem_nhdsWithin` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `closure` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_closure_image_mem_nhdsWithin` `instOrderTopologyOrderDual` `OrderDual.denselyOrdered` `dual`
`continuousWithinAt_left_of_exists_between` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `Set.instMembership` `Set.Ico`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_exists_between` `instOrderTopologyOrderDual` `dual`
`continuousWithinAt_left_of_image_mem_nhdsWithin` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_image_mem_nhdsWithin` `instOrderTopologyOrderDual` `OrderDual.denselyOrdered` `dual`
`continuousWithinAt_left_of_surjOn` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `Set.SurjOn` `Set.Iio`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_surjOn` `instOrderTopologyOrderDual` `dual`
`continuousWithinAt_right_of_closure_image_mem_nhdsWithin` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `closure` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin` `le_iff_le`
`continuousWithinAt_right_of_exists_between` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `Set.instMembership` `Set.Ioc`	`ContinuousWithinAt`	—	`mem_of_mem_nhdsWithin` `Set.self_mem_Ici` `tendsto_order` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `LT.lt.trans_le` `le_iff_le` `Ico_mem_nhdsGE` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `lt_iff_lt`
`continuousWithinAt_right_of_image_mem_nhdsWithin` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_closure_image_mem_nhdsWithin` `Filter.mem_of_superset` `subset_closure`
`continuousWithinAt_right_of_surjOn` 📖	mathematical	`StrictMonoOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `Set.SurjOn` `Set.Ioi`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_exists_between` `Eq.le`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_of_monotoneOn_of_closure_image_mem_nhds` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `closure` `Set.image`	`ContinuousAt`	—	`continuousAt_iff_continuous_left_right` `continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin` `mem_nhdsWithin_of_mem_nhds` `continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin`
`continuousAt_of_monotoneOn_of_exists_between` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `Set.Ioo`	`ContinuousAt`	—	`continuousAt_iff_continuous_left_right` `continuousWithinAt_left_of_monotoneOn_of_exists_between` `mem_nhdsWithin_of_mem_nhds` `continuousWithinAt_right_of_monotoneOn_of_exists_between`
`continuousAt_of_monotoneOn_of_image_mem_nhds` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhds` `Set.image`	`ContinuousAt`	—	`continuousAt_of_monotoneOn_of_closure_image_mem_nhds` `Filter.mem_of_superset` `subset_closure`
`continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `closure` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin` `instOrderTopologyOrderDual` `OrderDual.denselyOrdered` `MonotoneOn.dual`
`continuousWithinAt_left_of_monotoneOn_of_exists_between` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `Set.instMembership` `Set.Ioo`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_monotoneOn_of_exists_between` `instOrderTopologyOrderDual` `MonotoneOn.dual`
`continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin` `Filter.mem_of_superset` `subset_closure`
`continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `closure` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_monotoneOn_of_exists_between` `mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset` `exists_between` `mem_closure_iff` `LT.lt.le` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `LT.lt.trans_le`
`continuousWithinAt_right_of_monotoneOn_of_exists_between` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `Set.instMembership` `Set.Ioo`	`ContinuousWithinAt`	—	`mem_of_mem_nhdsWithin` `Set.self_mem_Ici` `tendsto_order` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `LT.lt.trans_le` `not_le` `LT.lt.not_ge` `Ico_mem_nhdsGE` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `LE.le.trans_lt` `LT.lt.le`
`continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ici` `Set.image`	`ContinuousWithinAt`	—	`continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin` `Filter.mem_of_superset` `subset_closure`

---

← Back to Index