LeftRightLim

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

Statistics

Metric	Count
Definitions `leftLim`, `rightLim`	2
Theorems `continuousAt_iff_leftLim_eq_rightLim`, `continuousWithinAt_Iio_iff_leftLim_eq`, `continuousWithinAt_Ioi_iff_rightLim_eq`, `le_leftLim`, `le_rightLim`, `leftLim`, `leftLim_le`, `leftLim_le_rightLim`, `rightLim`, `rightLim_le`, `rightLim_le_leftLim`, `tendsto_leftLim`, `tendsto_leftLim_within`, `tendsto_rightLim`, `tendsto_rightLim_within`, `leftLim_eq`, `rightLim_eq`, `continuousAt_iff_leftLim_eq_rightLim`, `continuousWithinAt_Iio_iff_leftLim_eq`, `continuousWithinAt_Ioi_iff_rightLim_eq`, `le_leftLim`, `le_rightLim`, `leftLim`, `leftLim_eq_sSup`, `leftLim_le`, `leftLim_le_rightLim`, `rightLim`, `rightLim_eq_sInf`, `rightLim_le`, `rightLim_le_leftLim`, `tendsto_leftLim`, `tendsto_leftLim_within`, `tendsto_rightLim`, `tendsto_rightLim_within`, `continuousWithinAt_leftLim_Iic`, `continuousWithinAt_rightLim_Ici`, `leftLim_eq_of_eq_bot`, `leftLim_eq_of_isBot`, `leftLim_eq_of_not_tendsto`, `leftLim_eq_of_tendsto`, `leftLim_leftLim`, `leftLim_rightLim`, `mapClusterPt_leftLim`, `mapClusterPt_rightLim`, `rightLim_eq_of_eq_bot`, `rightLim_eq_of_isTop`, `rightLim_eq_of_not_tendsto`, `rightLim_eq_of_tendsto`, `rightLim_leftLim`, `rightLim_rightLim`, `tendsto_atBot_of_mapClusterPt`, `tendsto_atTop_of_mapClusterPt`, `tendsto_leftLim_atBot_of_tendsto`, `tendsto_leftLim_atTop_of_tendsto`, `tendsto_leftLim_of_tendsto`, `tendsto_rightLim_atBot_of_tendsto`, `tendsto_rightLim_atTop_of_tendsto`, `tendsto_rightLim_of_tendsto`	58
Total	60

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_iff_leftLim_eq_rightLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousAt` `Function.leftLim` `Function.rightLim`	—	`Monotone.continuousAt_iff_leftLim_eq_rightLim` `instOrderTopologyOrderDual` `dual_right`
`continuousWithinAt_Iio_iff_leftLim_eq` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousWithinAt` `Set.Iio` `Function.leftLim`	—	`Monotone.continuousWithinAt_Iio_iff_leftLim_eq` `instOrderTopologyOrderDual` `dual_right`
`continuousWithinAt_Ioi_iff_rightLim_eq` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousWithinAt` `Set.Ioi` `Function.rightLim`	—	`Monotone.continuousWithinAt_Ioi_iff_rightLim_eq` `instOrderTopologyOrderDual` `dual_right`
`le_leftLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.leftLim`	—	`Monotone.leftLim_le` `instOrderTopologyOrderDual` `dual_right`
`le_rightLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.rightLim`	—	`Monotone.rightLim_le` `instOrderTopologyOrderDual` `dual_right`
`leftLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.leftLim`	—	`Monotone.leftLim` `instOrderTopologyOrderDual` `dual_right`
`leftLim_le` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.leftLim`	—	`Monotone.le_leftLim` `instOrderTopologyOrderDual` `dual_right`
`leftLim_le_rightLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.leftLim` `Function.rightLim`	—	`Monotone.rightLim_le_leftLim` `instOrderTopologyOrderDual` `dual_right`
`rightLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.rightLim`	—	`Monotone.rightLim` `instOrderTopologyOrderDual` `dual_right`
`rightLim_le` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.rightLim`	—	`Monotone.le_rightLim` `instOrderTopologyOrderDual` `dual_right`
`rightLim_le_leftLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.rightLim` `Function.leftLim`	—	`Monotone.leftLim_le_rightLim` `instOrderTopologyOrderDual` `dual_right`
`tendsto_leftLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `nhds` `Function.leftLim`	—	`Monotone.tendsto_leftLim` `instOrderTopologyOrderDual` `dual_right`
`tendsto_leftLim_within` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `Function.leftLim` `Set.Ici`	—	`Monotone.tendsto_leftLim_within` `instOrderTopologyOrderDual` `dual_right`
`tendsto_rightLim` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `nhds` `Function.rightLim`	—	`Monotone.tendsto_rightLim` `instOrderTopologyOrderDual` `dual_right`
`tendsto_rightLim_within` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `Function.rightLim` `Set.Iic`	—	`Monotone.tendsto_rightLim_within` `instOrderTopologyOrderDual` `dual_right`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftLim_eq` 📖	mathematical	`ContinuousWithinAt` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Function.leftLim`	—	`eq_or_ne` `leftLim_eq_of_eq_bot` `leftLim_eq_of_tendsto` `Filter.Tendsto.mono_left` `tendsto` `nhdsWithin_mono` `Set.Iio_subset_Iic_self`
`rightLim_eq` 📖	mathematical	`ContinuousWithinAt` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Function.rightLim`	—	`leftLim_eq` `instOrderTopologyOrderDual`

Function

Definitions

Name	Category	Theorems
`leftLim` 📖	CompOp	37 math math: `Monotone.continuousAt_iff_leftLim_eq_rightLim`, `Monotone.leftLim_eq_sSup`, `mapClusterPt_leftLim`, `Monotone.leftLim`, `leftLim_eq_of_eq_bot`, `Antitone.le_leftLim`, `StieltjesFunction.measure_Ioo`, `Monotone.rightLim_le_leftLim`, `StieltjesFunction.measure_singleton`, `StieltjesFunction.id_leftLim`, `tendsto_leftLim_of_tendsto`, `rightLim_leftLim`, `StieltjesFunction.countable_leftLim_ne`, `tendsto_leftLim_atBot_of_tendsto`, `StieltjesFunction.measure_Ici`, `Antitone.tendsto_leftLim`, `Antitone.continuousAt_iff_leftLim_eq_rightLim`, `Antitone.rightLim_le_leftLim`, `Monotone.continuousWithinAt_Iio_iff_leftLim_eq`, `Antitone.continuousWithinAt_Iio_iff_leftLim_eq`, `Antitone.leftLim`, `StieltjesFunction.measure_Icc`, `Antitone.tendsto_leftLim_within`, `ContinuousWithinAt.leftLim_eq`, `Antitone.leftLim_le`, `Monotone.tendsto_leftLim_within`, `leftLim_eq_of_tendsto`, `StieltjesFunction.measure_Iio`, `leftLim_eq_of_not_tendsto`, `Antitone.leftLim_le_rightLim`, `Monotone.leftLim_le`, `StieltjesFunction.measure_Ico`, `leftLim_eq_of_isBot`, `tendsto_leftLim_atTop_of_tendsto`, `Monotone.le_leftLim`, `Monotone.tendsto_leftLim`, `Monotone.leftLim_le_rightLim`
`rightLim` 📖	CompOp	31 math math: `Monotone.continuousAt_iff_leftLim_eq_rightLim`, `StieltjesFunction.rightLim_eq`, `Antitone.tendsto_rightLim`, `Monotone.rightLim_le_leftLim`, `Monotone.rightLim_eq_sInf`, `tendsto_rightLim_atBot_of_tendsto`, `mapClusterPt_rightLim`, `ContinuousWithinAt.rightLim_eq`, `Antitone.continuousAt_iff_leftLim_eq_rightLim`, `Antitone.rightLim_le_leftLim`, `rightLim_eq_of_not_tendsto`, `Monotone.continuousWithinAt_Ioi_iff_rightLim_eq`, `rightLim_eq_of_eq_bot`, `Monotone.rightLim_le`, `Antitone.tendsto_rightLim_within`, `Antitone.le_rightLim`, `Monotone.tendsto_rightLim`, `Antitone.rightLim`, `tendsto_rightLim_atTop_of_tendsto`, `Monotone.le_rightLim`, `leftLim_rightLim`, `tendsto_rightLim_of_tendsto`, `Antitone.rightLim_le`, `Antitone.leftLim_le_rightLim`, `rightLim_eq_of_isTop`, `Monotone.tendsto_rightLim_within`, `Monotone.rightLim`, `Monotone.stieltjesFunction_eq`, `Antitone.continuousWithinAt_Ioi_iff_rightLim_eq`, `rightLim_eq_of_tendsto`, `Monotone.leftLim_le_rightLim`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_iff_leftLim_eq_rightLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousAt` `Function.leftLim` `Function.rightLim`	—	`continuousWithinAt_Iio_iff_leftLim_eq` `ContinuousAt.continuousWithinAt` `continuousWithinAt_Ioi_iff_rightLim_eq` `le_antisymm` `leftLim_le` `le_refl` `le_rightLim` `continuousAt_iff_continuous_left'_right'`
`continuousWithinAt_Iio_iff_leftLim_eq` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousWithinAt` `Set.Iio` `Function.leftLim`	—	`eq_or_ne` `leftLim_eq_of_eq_bot` `tendsto_nhds_unique` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `Filter.neBot_iff` `tendsto_leftLim` `ContinuousWithinAt.tendsto`
`continuousWithinAt_Ioi_iff_rightLim_eq` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`ContinuousWithinAt` `Set.Ioi` `Function.rightLim`	—	`continuousWithinAt_Iio_iff_leftLim_eq` `instOrderTopologyOrderDual` `dual`
`le_leftLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.leftLim`	—	`eq_or_ne` `leftLim_eq_of_eq_bot` `LT.lt.le` `leftLim_eq_sSup` `le_csSup` `Set.mem_image_of_mem`
`le_rightLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.rightLim`	—	`leftLim_le` `instOrderTopologyOrderDual` `dual`
`leftLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.leftLim`	—	`eq_or_lt_of_le` `le_rfl` `LE.le.trans` `leftLim_le` `le_leftLim`
`leftLim_eq_sSup` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.leftLim` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image` `Set.Iio`	—	`leftLim_eq_of_tendsto` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `tendsto_nhdsLT`
`leftLim_le` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.leftLim`	—	`eq_or_ne` `supSet_to_nonempty` `leftLim_eq_sSup` `csSup_le` `Filter.forall_mem_nonempty_iff_neBot` `Filter.neBot_iff` `self_mem_nhdsWithin` `LE.le.trans` `LT.lt.le`
`leftLim_le_rightLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Function.leftLim` `Function.rightLim`	—	`LE.le.trans` `leftLim_le` `le_rfl` `le_rightLim`
`rightLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.rightLim`	—	`leftLim` `instOrderTopologyOrderDual` `dual`
`rightLim_eq_sInf` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Function.rightLim` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image` `Set.Ioi`	—	`rightLim_eq_of_tendsto` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `tendsto_nhdsGT`
`rightLim_le` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.rightLim`	—	`le_leftLim` `instOrderTopologyOrderDual` `dual`
`rightLim_le_leftLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLT`	`Preorder.toLE` `Function.rightLim` `Function.leftLim`	—	`Filter.eq_or_neBot` `supSet_to_nonempty` `rightLim_le` `Filter.nonempty_of_mem` `Ioo_mem_nhdsLT` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `le_leftLim`
`tendsto_leftLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `nhds` `Function.leftLim`	—	`tendsto_leftLim_of_tendsto` `tendsto_nhdsLT`
`tendsto_leftLim_within` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `Function.leftLim` `Set.Iic`	—	`tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `tendsto_leftLim` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `le_leftLim`
`tendsto_rightLim` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `nhds` `Function.rightLim`	—	`tendsto_leftLim` `instOrderTopologyOrderDual` `dual`
`tendsto_rightLim_within` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `Function.rightLim` `Set.Ici`	—	`tendsto_leftLim_within` `instOrderTopologyOrderDual` `dual`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousWithinAt_leftLim_Iic` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.leftLim`	`ContinuousWithinAt` `Set.Iic`	—	`Set.Iio_union_Icc_eq_Iic` `le_rfl` `nhdsWithin_union` `Set.Icc_self` `nhdsWithin_singleton` `ContinuousWithinAt.eq_1` `Filter.tendsto_sup` `Filter.HasBasis.tendsto_right_iff` `closed_nhds_basis` `T3Space.toRegularSpace` `Filter.eq_or_neBot` `Filter.nonempty_of_mem` `self_mem_nhdsWithin` `mem_nhdsLT_iff_exists_Ioo_subset'` `Filter.mp_mem` `Ioo_mem_nhdsLT` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Filter.univ_mem'` `leftLim_eq_of_eq_bot` `leftLim_eq_of_not_tendsto` `IsClosed.mem_of_tendsto` `tendsto_leftLim_of_tendsto` `Ioo_mem_nhdsLT_of_mem` `LT.lt.le`
`continuousWithinAt_rightLim_Ici` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.rightLim`	`ContinuousWithinAt` `Set.Ici`	—	`continuousWithinAt_leftLim_Iic` `instOrderTopologyOrderDual`
`leftLim_eq_of_eq_bot` 📖	mathematical	`nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `Filter` `Filter.instBot`	`Function.leftLim`	—	`OrderTopology.topology_eq_generate_intervals`
`leftLim_eq_of_isBot` 📖	mathematical	`IsBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Function.leftLim`	—	`leftLim_eq_of_eq_bot` `nhdsWithin_empty`
`leftLim_eq_of_not_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.leftLim`	—	`OrderTopology.topology_eq_generate_intervals`
`leftLim_eq_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.leftLim`	—	`OrderTopology.topology_eq_generate_intervals` `lim_eq` `Filter.map_neBot` `Filter.neBot_iff`
`leftLim_leftLim` 📖	—	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.leftLim`	—	—	`ContinuousWithinAt.leftLim_eq` `T25Space.t2Space` `T3Space.t25Space` `continuousWithinAt_leftLim_Iic`
`leftLim_rightLim` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.leftLim`	`Function.rightLim`	—	`Filter.nonempty_of_mem` `self_mem_nhdsWithin` `leftLim_eq_of_tendsto` `T25Space.t2Space` `T3Space.t25Space` `Filter.neBot_iff` `Filter.HasBasis.tendsto_right_iff` `closed_nhds_basis` `T3Space.toRegularSpace` `mem_nhdsLT_iff_exists_Ioo_subset'` `Filter.mp_mem` `Ioo_mem_nhdsLT` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Filter.univ_mem'` `Filter.eq_or_neBot` `rightLim_eq_of_eq_bot` `rightLim_eq_of_not_tendsto` `IsClosed.mem_of_tendsto` `tendsto_rightLim_of_tendsto` `Ioo_mem_nhdsGT_of_mem` `instClosedIciTopology` `LT.lt.le`
`mapClusterPt_leftLim` 📖	mathematical	—	`MapClusterPt` `Function.leftLim` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Filter.inf_neBot_iff` `mem_of_mem_nhds` `mem_of_mem_nhdsWithin` `Set.self_mem_Iic` `Filter.eq_or_neBot` `leftLim_eq_of_eq_bot` `leftLim_eq_of_not_tendsto` `Filter.Tendsto.mapClusterPt` `tendsto_leftLim_of_tendsto` `MapClusterPt.mono` `nhdsWithin_mono` `Set.Iio_subset_Iic_self`
`mapClusterPt_rightLim` 📖	mathematical	—	`MapClusterPt` `Function.rightLim` `nhdsWithin` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`mapClusterPt_leftLim` `instOrderTopologyOrderDual`
`rightLim_eq_of_eq_bot` 📖	mathematical	`nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `Filter` `Filter.instBot`	`Function.rightLim`	—	`leftLim_eq_of_eq_bot` `instOrderTopologyOrderDual`
`rightLim_eq_of_isTop` 📖	mathematical	`IsTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Function.rightLim`	—	`leftLim_eq_of_isBot`
`rightLim_eq_of_not_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.rightLim`	—	`leftLim_eq_of_not_tendsto` `instOrderTopologyOrderDual`
`rightLim_eq_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.rightLim`	—	`leftLim_eq_of_tendsto` `instOrderTopologyOrderDual`
`rightLim_leftLim` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.rightLim`	`Function.leftLim`	—	`leftLim_rightLim` `instOrderTopologyOrderDual`
`rightLim_rightLim` 📖	—	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Function.rightLim`	—	—	`leftLim_leftLim` `instOrderTopologyOrderDual`
`tendsto_atBot_of_mapClusterPt` 📖	—	`Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Filter.Eventually` `MapClusterPt`	—	—	`tendsto_atTop_of_mapClusterPt` `instOrderTopologyOrderDual` `OrderDual.noTopOrder`
`tendsto_atTop_of_mapClusterPt` 📖	—	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Filter.Eventually` `MapClusterPt`	—	—	`isEmpty_or_nonempty` `Filter.filter_eq_bot_of_isEmpty` `Filter.HasBasis.tendsto_right_iff` `closed_nhds_basis` `T3Space.toRegularSpace` `SemilatticeSup.instIsDirectedOrder` `Filter.Eventually.and` `Filter.mp_mem` `Filter.Ioi_mem_atTop` `Filter.univ_mem'` `IsClosed.mem_of_mapClusterPt` `LT.lt.le` `Ici_mem_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology`
`tendsto_leftLim_atBot_of_tendsto` 📖	mathematical	`Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.leftLim`	—	`tendsto_rightLim_atTop_of_tendsto` `instOrderTopologyOrderDual`
`tendsto_leftLim_atTop_of_tendsto` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.leftLim`	—	`tendsto_atTop_of_mapClusterPt` `Filter.Eventually.of_forall` `MapClusterPt.mono` `mapClusterPt_leftLim` `nhdsWithin_le_nhds`
`tendsto_leftLim_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.leftLim`	—	`Filter.eq_or_neBot` `OrderTopology.topology_eq_generate_intervals` `Filter.neBot_iff` `tendsto_nhds_limUnder`
`tendsto_rightLim_atBot_of_tendsto` 📖	mathematical	`Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.rightLim`	—	`tendsto_leftLim_atTop_of_tendsto` `instOrderTopologyOrderDual` `OrderDual.noTopOrder`
`tendsto_rightLim_atTop_of_tendsto` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.rightLim`	—	`Filter.OrderTop.atTop_eq` `rightLim_eq_of_isTop` `isTop_top` `tendsto_nhds_unique` `T25Space.t2Space` `T3Space.t25Space` `Filter.pure_neBot` `tendsto_pure_nhds` `tendsto_atTop_of_mapClusterPt` `Filter.Eventually.of_forall` `MapClusterPt.mono` `mapClusterPt_rightLim` `nhdsWithin_le_nhds`
`tendsto_rightLim_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Function.rightLim`	—	`tendsto_leftLim_of_tendsto` `instOrderTopologyOrderDual`

---

← Back to Index