Basic

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

Statistics

Metric	Count
Definitions OrderTopology, topology	2
Theorems topology_eq_generateFrom, exists_Ioo_subset, squeeze, squeeze', isClosed, isOpen, exists_Ioo_subset, isClosed, isOpen, continuousWithinAt_Iic, isEmbedding_of_ordConnected, continuous_iff, to_orderClosedTopology, topology_eq_generate_intervals, hasBasis_nhds_Ioc, hasBasis_nhds_Ioc_of_exists_gt, continuousWithinAt_Ici, of_separableSpace_orderTopology, countable_of_Ioo, induced_topology_eq_preorder, isEmbedding_of_ordConnected, hasBasis_nhds_Ioc, hasBasis_nhds_Ioc_of_exists_lt, countable_image_gt_image_Iio, countable_image_gt_image_Iio_within, countable_image_gt_image_Ioi, countable_image_gt_image_Ioi_within, countable_image_lt_image_Iio, countable_image_lt_image_Iio_within, countable_image_lt_image_Ioi, countable_image_lt_image_Ioi_within, countable_of_isolated_left', countable_setOf_covBy_left, countable_setOf_covBy_right, dense_iff_exists_between, dense_of_exists_between, exists_Icc_mem_subset_of_mem_nhds, exists_Icc_mem_subset_of_mem_nhdsGE, exists_Icc_mem_subset_of_mem_nhdsLE, exists_Ico_subset_of_mem_nhds, exists_Ico_subset_of_mem_nhds', exists_Ioc_subset_of_mem_nhds, exists_Ioc_subset_of_mem_nhds', exists_countable_generateFrom_Ioi_Iio, ge_mem_nhds, gt_mem_nhds, induced_orderTopology, induced_orderTopology', induced_topology_eq_preorder, induced_topology_le_preorder, instIsCountablyGenerated_atBot, instIsCountablyGenerated_atTop, instOrderTopologyOrderDual, instSecondCountableTopologyOfOrderTopologyOfCountable, isOpen_Iio', isOpen_Ioi', isOpen_gt', isOpen_iff_generate_intervals, isOpen_lt', isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom, le_mem_nhds, lt_mem_nhds, mem_nhds_iff_exists_Ioo_subset, mem_nhds_iff_exists_Ioo_subset', nhdsGE_basis, nhdsGE_basis_of_exists_gt, nhdsGE_eq_iInf_inf_principal, nhdsGE_eq_iInf_principal, nhdsLE_basis, nhdsLE_basis_of_exists_lt, nhdsLE_eq_iInf_inf_principal, nhdsLE_eq_iInf_principal, nhds_basis_Ioo, nhds_basis_Ioo', nhds_bot_basis, nhds_bot_basis_Iic, nhds_bot_order, nhds_eq_order, nhds_order_unbounded, nhds_top_basis, nhds_top_basis_Ici, nhds_top_order, orderTopology_of_ordConnected, order_separated, pi_Icc_mem_nhds, pi_Icc_mem_nhds', pi_Ici_mem_nhds, pi_Ici_mem_nhds', pi_Ico_mem_nhds, pi_Ico_mem_nhds', pi_Iic_mem_nhds, pi_Iic_mem_nhds', pi_Iio_mem_nhds, pi_Iio_mem_nhds', pi_Ioc_mem_nhds, pi_Ioc_mem_nhds', pi_Ioi_mem_nhds, pi_Ioi_mem_nhds', pi_Ioo_mem_nhds, pi_Ioo_mem_nhds', tendstoIccClassNhds, tendstoIccClassNhdsPi, tendstoIcoClassNhds, tendstoIocClassNhds, tendstoIooClassNhds, tendstoIxxNhdsWithin, tendsto_nhds_bot_mono, tendsto_nhds_bot_mono', tendsto_nhds_top_mono, tendsto_nhds_top_mono', tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_of_tendsto_of_tendsto_of_le_of_le', tendsto_order, tendsto_order_unbounded	114
Total	116

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topology_eq_generateFrom 📖	mathematical	Dense	TopologicalSpace.generateFrom Set Set.instUnion Set.image Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iio	—	OrderTopology.topology_eq_generate_intervals le_antisymm TopologicalSpace.generateFrom_anti le_generateFrom Ioi_eq_biUnion OrderTopology.to_orderClosedTopology isOpen_iUnion Set.mem_image_of_mem Iio_eq_biUnion

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_Ioo_subset 📖	mathematical	Filter.Eventually nhds	Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instHasSubset setOf	—	mem_nhds_iff_exists_Ioo_subset

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
squeeze 📖	—	Filter.Tendsto nhds Pi.hasLe Preorder.toLE	—	—	tendsto_of_tendsto_of_tendsto_of_le_of_le
squeeze' 📖	—	Filter.Tendsto nhds Filter.Eventually Preorder.toLE	—	—	tendsto_of_tendsto_of_tendsto_of_le_of_le'

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed 📖	mathematical	IsLowerSet Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsClosed	—	IsUpperSet.isClosed instOrderTopologyOrderDual IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT toDual
isOpen 📖	mathematical	IsLowerSet Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsOpen	—	IsUpperSet.isClosed compl

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_Ioo_subset 📖	mathematical	IsOpen Set.Nonempty	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instHasSubset Set.Ioo	—	exists_ne lt_trichotomy exists_Ico_subset_of_mem_nhds mem_nhds HasSubset.Subset.trans Set.instIsTransSubset Set.Ioo_subset_Ico_self exists_Ioc_subset_of_mem_nhds Set.Ioo_subset_Ioc_self

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed 📖	mathematical	IsUpperSet Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsClosed	—	eq_empty_or_Ici isClosed_empty isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology
isOpen 📖	mathematical	IsUpperSet Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsOpen	—	IsLowerSet.isOpen instOrderTopologyOrderDual IsWellOrder.toIsWellFounded isWellOrder_lt instWellFoundedLTOrderDualOfWellFoundedGT toDual

LeftOrdContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousWithinAt_Iic 📖	mathematical	LeftOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	ContinuousWithinAt Set.Iic	—	ContinuousWithinAt.eq_1 OrderTopology.topology_eq_generate_intervals lt_isLUB_iff isLUB_Iio isOpen_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology LT.lt.trans_le mono LT.lt.le isOpen_univ LE.le.trans_lt

OrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmbedding_of_ordConnected 📖	mathematical	—	Topology.IsEmbedding DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderEmbedding	—	StrictMono.isEmbedding_of_ordConnected strictMono

OrderTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_iff 📖	mathematical	—	Continuous IsOpen Set.preimage Set.Ioi Set.Iio	—	topology_eq_generate_intervals
to_orderClosedTopology 📖	mathematical	—	OrderClosedTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isOpen_compl_iff isOpen_prod_iff lt_of_not_ge order_separated not_le_of_gt
topology_eq_generate_intervals 📖	mathematical	—	TopologicalSpace.generateFrom setOf Set Set.Ioi Set.Iio	—	—

PredOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_nhds_Ioc 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ico	—	hasBasis_nhds_Ioc_of_exists_gt NoMaxOrder.exists_gt
hasBasis_nhds_Ioc_of_exists_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhds Set.Ico	—	nhdsGE_basis_of_exists_gt nhdsGE_eq_nhds instClosedIicTopology OrderTopology.to_orderClosedTopology

Preorder

Definitions

Name	Category	Theorems
topology 📖	CompOp	4 math math: StrictMono.induced_topology_eq_preorder, MeasureTheory.Filtration.rightCont_def, induced_topology_eq_preorder, induced_topology_le_preorder

RightOrdContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousWithinAt_Ici 📖	mathematical	RightOrdContinuous PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	ContinuousWithinAt Set.Ici	—	LeftOrdContinuous.continuousWithinAt_Iic instOrderTopologyOrderDual OrderDual.denselyOrdered orderDual

SecondCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_separableSpace_orderTopology 📖	mathematical	—	SecondCountableTopology	—	TopologicalSpace.exists_countable_dense Set.Countable.union Set.Countable.image Dense.topology_eq_generateFrom

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_of_Ioo 📖	mathematical	Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set.Countable	—	countable_of_isOpen TopologicalSpace.SecondCountableTopology.to_separableSpace subset Set.diff_subset isOpen_Ioo OrderTopology.to_orderClosedTopology LT.lt.exists_lt_lt Set.Countable.of_diff countable_setOf_covBy_right

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induced_topology_eq_preorder 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	TopologicalSpace.induced Preorder.topology	—	induced_topology_eq_preorder lt_iff_lt Set.OrdConnected.out Set.mem_range_self not_lt LT.lt.le le_rfl
isEmbedding_of_ordConnected 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Topology.IsEmbedding	—	OrderTopology.topology_eq_generate_intervals induced_topology_eq_preorder injective

SuccOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_nhds_Ioc 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioc	—	hasBasis_nhds_Ioc_of_exists_lt NoMinOrder.exists_lt
hasBasis_nhds_Ioc_of_exists_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhds Set.Ioc	—	nhdsLE_basis_of_exists_lt nhdsLE_eq_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology

(root)

Definitions

Name	Category	Theorems
OrderTopology 📖	CompData	19 math math: orderTopology_of_nhds_mabs, orderTopology_of_nhds_abs, TopologicalSpace.instOrderTopologyWithTop, ENat.instOrderTopology, Rat.instOrderTopology, Irrational.instOrderTopologySubtypeReal, induced_orderTopology', instOrderTopologyReal, Ordinal.instOrderTopology, NNReal.instOrderTopology, ENNReal.instOrderTopology, NNRat.instOrderTopology, instOrderTopologyOrderDual, OrderTopology.of_discreteTopology, OrderTopology.of_linearLocallyFinite, orderTopology_of_ordConnected, discreteTopology_iff_orderTopology_of_pred_succ, EReal.instOrderTopology, induced_orderTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_image_gt_image_Iio 📖	mathematical	—	Set.Countable setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_image_gt_image_Iio_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi_within instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_image_gt_image_Ioi 📖	mathematical	—	Set.Countable setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_image_gt_image_Ioi_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi_within instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_image_lt_image_Iio 📖	mathematical	—	Set.Countable setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi
countable_image_lt_image_Iio_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi_within
countable_image_lt_image_Ioi 📖	mathematical	—	Set.Countable setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	countable_image_lt_image_Ioi_within
countable_image_lt_image_Ioi_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim instIsEmptyFalse Nonempty.map Nontrivial.to_nonempty StrictMonoOn.injOn LE.le.lt_of_ne Set.disjoint_iff_forall_ne lt_irrefl LT.lt.trans LT.lt.trans_le Set.InjOn.leftInvOn_invFunOn Disjoint.symm le_of_not_ge Set.PairwiseDisjoint.countable_of_Ioo Set.MapsTo.countable_of_injOn Set.mapsTo_image Function.sometimes_spec
countable_of_isolated_left' 📖	mathematical	—	Set.Countable setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.Ioo Set.instEmptyCollection	—	countable_setOf_covBy_left
countable_setOf_covBy_left 📖	mathematical	—	Set.Countable setOf CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	toDual_covBy_toDual_iff countable_setOf_covBy_right instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_setOf_covBy_right 📖	mathematical	—	Set.Countable setOf CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim CovBy.le_of_lt exists_Ioc_subset_of_mem_nhds IsOpen.mem_nhds Ne.lt_or_gt Set.disjoint_left LT.lt.trans_le LE.le.trans CovBy.le lt_irrefl LE.le.trans_lt Set.PairwiseDisjoint.countable_of_isOpen TopologicalSpace.SecondCountableTopology.to_separableSpace Set.Subset.antisymm Set.Ioc_subset_Ioo_right CovBy.lt isOpen_Ioo OrderTopology.to_orderClosedTopology le_rfl Function.sometimes_spec Set.Countable.of_diff Set.Subsingleton.countable Set.subsingleton_isBot TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne T2Space.t1Space OrderClosedTopology.to_t2Space TopologicalSpace.isBasis_countableBasis CovBy.ne Set.mem_iUnion₂ Set.Countable.mono Set.Countable.biUnion TopologicalSpace.countable_countableBasis TopologicalSpace.isOpen_of_mem_countableBasis
dense_iff_exists_between 📖	mathematical	—	Dense Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Dense.exists_between OrderTopology.to_orderClosedTopology dense_of_exists_between
dense_of_exists_between 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Dense	—	dense_iff_inter_open IsOpen.exists_Ioo_subset
exists_Icc_mem_subset_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.instMembership Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instHasSubset	—	exists_Icc_mem_subset_of_mem_nhdsLE nhdsWithin_le_nhds exists_Icc_mem_subset_of_mem_nhdsGE Set.Icc_union_Icc_eq_Icc nhdsLE_sup_nhdsGE Filter.union_mem_sup Set.union_subset
exists_Icc_mem_subset_of_mem_nhdsGE 📖	mathematical	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE Set.Icc Set.instHasSubset	—	not_isMax_iff em IsMax.Ici_eq nhdsWithin_singleton Set.Icc_self Filter.HasBasis.mem_iff nhdsGE_basis_of_exists_gt Set.eq_empty_or_nonempty Set.Icc_union_Ioo_eq_Ico le_rfl Set.union_empty Ico_mem_nhdsGE instClosedIciTopology OrderTopology.to_orderClosedTopology LT.lt.le Icc_mem_nhdsGE HasSubset.Subset.trans Set.instIsTransSubset Set.Icc_subset_Ico_right
exists_Icc_mem_subset_of_mem_nhdsLE 📖	mathematical	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE Set.Icc Set.instHasSubset	—	Function.Surjective.exists Equiv.surjective Set.Icc_toDual exists_Icc_mem_subset_of_mem_nhdsGE instOrderTopologyOrderDual
exists_Ico_subset_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.instHasSubset Set.Ico	—	exists_Ico_subset_of_mem_nhds'
exists_Ico_subset_of_mem_nhds' 📖	mathematical	Set Filter Filter.instMembership nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.instMembership Set.Ioc Set.instHasSubset Set.Ico	—	Set.Ico_toDual Set.Ioc_toDual exists_Ioc_subset_of_mem_nhds' instOrderTopologyOrderDual LT.lt.dual
exists_Ioc_subset_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.instHasSubset Set.Ioc	—	Filter.HasBasis.mem_iff nhdsLE_basis_of_exists_lt nhdsWithin_le_nhds
exists_Ioc_subset_of_mem_nhds' 📖	mathematical	Set Filter Filter.instMembership nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set.instMembership Set.Ico Set.instHasSubset Set.Ioc	—	exists_Ioc_subset_of_mem_nhds le_max_left max_lt HasSubset.Subset.trans Set.instIsTransSubset Set.Ioc_subset_Ioc_left le_max_right
exists_countable_generateFrom_Ioi_Iio 📖	mathematical	—	Set.Countable TopologicalSpace.generateFrom setOf Set Set.instMembership Set.Ioi Set.Iio	—	isEmpty_or_nonempty Unique.instSubsingleton IsEmpty.instSubsingleton TopologicalSpace.exists_countable_of_generateFrom OrderTopology.topology_eq_generate_intervals Set.Countable.image le_antisymm TopologicalSpace.le_generateFrom_iff_subset_isOpen TopologicalSpace.generateFrom_anti Function.sometimes_spec
ge_mem_nhds 📖	mathematical	Preorder.toLT	Filter.Eventually Preorder.toLE nhds	—	Filter.Eventually.mono gt_mem_nhds le_of_lt
gt_mem_nhds 📖	mathematical	Preorder.toLT	Filter.Eventually nhds	—	IsOpen.mem_nhds isOpen_gt'
induced_orderTopology 📖	mathematical	Preorder.toLT	OrderTopology TopologicalSpace.induced	—	induced_orderTopology' le_of_lt
induced_orderTopology' 📖	mathematical	Preorder.toLT Preorder.toLE	OrderTopology TopologicalSpace.induced	—	induced_topology_eq_preorder
induced_topology_eq_preorder 📖	mathematical	Preorder.toLT Preorder.toLE	TopologicalSpace.induced Preorder.topology	—	le_antisymm induced_topology_le_preorder le_of_nhds_le_nhds nhds_eq_order nhds_induced Filter.comap_inf Filter.comap_iInf iInf_congr_Prop Filter.comap_principal inf_le_inf le_iInf₂ iInf₂_le_of_le Filter.principal_mono LE.le.trans_lt Filter.le_principal_iff Filter.univ_mem' LT.lt.trans_le
induced_topology_le_preorder 📖	mathematical	Preorder.toLT	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.induced Preorder.topology	—	le_of_nhds_le_nhds nhds_induced nhds_eq_order iInf_congr_Prop Filter.comap_inf Filter.comap_iInf Filter.comap_principal inf_le_inf le_iInf₂ iInf₂_le
instIsCountablyGenerated_atBot 📖	mathematical	—	Filter.IsCountablyGenerated Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	instIsCountablyGenerated_atTop instOrderTopologyOrderDual instSeparableSpaceOrderDual
instIsCountablyGenerated_atTop 📖	mathematical	—	Filter.IsCountablyGenerated Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.eq_empty_or_nonempty TopologicalSpace.exists_countable_dense Filter.atTop_eq_generate_of_not_bddAbove Dense.exists_mem_open isOpen_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology LE.le.not_gt Set.Countable.image Filter.atTop_eq_pure_of_isTop Filter.isCountablyGenerated_pure
instOrderTopologyOrderDual 📖	mathematical	—	OrderTopology OrderDual OrderDual.instTopologicalSpace OrderDual.instPreorder	—	OrderTopology.topology_eq_generate_intervals
instSecondCountableTopologyOfOrderTopologyOfCountable 📖	mathematical	—	SecondCountableTopology	—	Set.Countable.mono Set.Countable.union Set.countable_range OrderTopology.topology_eq_generate_intervals
isOpen_Iio' 📖	mathematical	—	IsOpen Set.Iio	—	isOpen_gt'
isOpen_Ioi' 📖	mathematical	—	IsOpen Set.Ioi	—	isOpen_lt'
isOpen_gt' 📖	mathematical	—	IsOpen setOf Preorder.toLT	—	isOpen_iff_generate_intervals
isOpen_iff_generate_intervals 📖	mathematical	—	IsOpen TopologicalSpace.GenerateOpen setOf Set Set.Ioi Set.Iio	—	OrderTopology.topology_eq_generate_intervals
isOpen_lt' 📖	mathematical	—	IsOpen setOf Preorder.toLT	—	isOpen_iff_generate_intervals
isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom 📖	mathematical	TopologicalSpace.generateFrom setOf Set Set.instMembership Set.Ioi Set.Iio	TopologicalSpace.IsTopologicalBasis Set.instHasSubset Set.Finite Set.instInter Set.iInter	—	TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset IsOpen.inter Set.Finite.isOpen_biInter TopologicalSpace.isOpen_generateFrom_of_mem TopologicalSpace.isTopologicalBasis_of_subbasis Set.ext Set.Finite.subset Set.finite_range Set.sInter_eq_biInter Set.biInter_union Set.biInter_range Set.biInter_eq_iInter Set.iInter_coe_set
le_mem_nhds 📖	mathematical	Preorder.toLT	Filter.Eventually Preorder.toLE nhds	—	Filter.Eventually.mono lt_mem_nhds le_of_lt
lt_mem_nhds 📖	mathematical	Preorder.toLT	Filter.Eventually nhds	—	IsOpen.mem_nhds isOpen_lt'
mem_nhds_iff_exists_Ioo_subset 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instHasSubset	—	mem_nhds_iff_exists_Ioo_subset' NoMinOrder.exists_lt NoMaxOrder.exists_gt
mem_nhds_iff_exists_Ioo_subset' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Set.instMembership Set.Ioo Set.instHasSubset	—	exists_Ico_subset_of_mem_nhds exists_Ioc_subset_of_mem_nhds Set.union_subset Set.Ioc_union_Ico_eq_Ioo Filter.mem_of_superset Ioo_mem_nhds OrderTopology.to_orderClosedTopology
nhdsGE_basis 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ico	—	nhdsGE_basis_of_exists_gt NoMaxOrder.exists_gt
nhdsGE_basis_of_exists_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhdsWithin Set.Ici Set.Ico	—	Filter.hasBasis_biInf_principal lt_min Set.Ico_subset_Ico_right min_le_left min_le_right nhdsGE_eq_iInf_principal
nhdsGE_eq_iInf_inf_principal 📖	mathematical	—	nhdsWithin Set.Ici Filter Filter.instInf iInf Filter.instInfSet Preorder.toLT Filter.principal Set.Iio	—	nhdsWithin.eq_1 nhds_eq_order le_antisymm inf_le_inf_right inf_le_right le_inf LE.le.trans le_iInf₂ Filter.principal_mono Set.Ici_subset_Ioi inf_le_left
nhdsGE_eq_iInf_principal 📖	mathematical	Preorder.toLT	nhdsWithin Set.Ici iInf Filter Filter.instInfSet Filter.principal Set.Ico	—	nhdsGE_eq_iInf_inf_principal biInf_inf iInf_congr_Prop Filter.inf_principal Set.Iio_inter_Ici
nhdsLE_basis 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioc	—	nhdsLE_basis_of_exists_lt NoMinOrder.exists_lt
nhdsLE_basis_of_exists_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhdsWithin Set.Iic Set.Ioc	—	Set.Ico_toDual nhdsGE_basis_of_exists_gt instOrderTopologyOrderDual
nhdsLE_eq_iInf_inf_principal 📖	mathematical	—	nhdsWithin Set.Iic Filter Filter.instInf iInf Filter.instInfSet Preorder.toLT Filter.principal Set.Ioi	—	nhdsGE_eq_iInf_inf_principal instOrderTopologyOrderDual
nhdsLE_eq_iInf_principal 📖	mathematical	Preorder.toLT	nhdsWithin Set.Iic iInf Filter Filter.instInfSet Filter.principal Set.Ioc	—	nhdsLE_eq_iInf_inf_principal biInf_inf iInf_congr_Prop Filter.inf_principal
nhds_basis_Ioo 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioo	—	nhds_basis_Ioo' NoMinOrder.exists_lt NoMaxOrder.exists_gt
nhds_basis_Ioo' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhds Set.Ioo	—	mem_nhds_iff_exists_Ioo_subset'
nhds_bot_basis 📖	mathematical	—	Filter.HasBasis nhds Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Iio	—	nhds_top_basis instOrderTopologyOrderDual OrderDual.instNontrivial
nhds_bot_basis_Iic 📖	mathematical	—	Filter.HasBasis nhds Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Iic	—	nhds_top_basis_Ici instOrderTopologyOrderDual OrderDual.instNontrivial OrderDual.denselyOrdered
nhds_bot_order 📖	mathematical	—	nhds Bot.bot OrderBot.toBot Preorder.toLE iInf Filter Filter.instInfSet Preorder.toLT Filter.principal Set.Iio	—	nhds_eq_order iInf_congr_Prop IsMin.Iio_eq iInf_neg iInf_top inf_of_le_right
nhds_eq_order 📖	mathematical	—	nhds Filter Filter.instInf iInf Filter.instInfSet Set Set.instMembership Set.Iio Filter.principal Set.Ioi	—	OrderTopology.topology_eq_generate_intervals TopologicalSpace.nhds_generateFrom iInf_congr_Prop iInf_or iInf_and iInf_exists iInf_inf_eq iInf_comm iInf_iInf_eq_left
nhds_order_unbounded 📖	mathematical	Preorder.toLT	nhds iInf Filter Filter.instInfSet Filter.principal Set.Ioo	—	nhds_eq_order iInf_congr_Prop
nhds_top_basis 📖	mathematical	—	Filter.HasBasis nhds Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioi	—	Ne.lt_top exists_ne Set.Iic_top nhdsWithin_univ Set.Ioc_top nhdsLE_basis_of_exists_lt
nhds_top_basis_Ici 📖	mathematical	—	Filter.HasBasis nhds Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ici	—	Filter.HasBasis.to_hasBasis nhds_top_basis exists_between Set.Ici_subset_Ioi Set.Ioi_subset_Ici_self
nhds_top_order 📖	mathematical	—	nhds Top.top OrderTop.toTop Preorder.toLE iInf Filter Filter.instInfSet Preorder.toLT Filter.principal Set.Ioi	—	nhds_eq_order iInf_congr_Prop IsMax.Ioi_eq iInf_neg iInf_top inf_of_le_left
orderTopology_of_ordConnected 📖	mathematical	—	OrderTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership Subtype.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	StrictMono.induced_topology_eq_preorder Subtype.strictMono_coe Subtype.range_val
order_separated 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsOpen Set Set.instMembership	—	LT.lt.exists_disjoint_Iio_Ioi isOpen_gt' isOpen_lt'
pi_Icc_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Icc Pi.preorder	—	set_pi_mem_nhds Set.finite_univ Icc_mem_nhds OrderTopology.to_orderClosedTopology Set.pi_univ_Icc
pi_Icc_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Icc Pi.preorder	—	pi_Icc_mem_nhds
pi_Ici_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ici Pi.preorder	—	set_pi_mem_nhds Set.toFinite Subtype.finite Ici_mem_nhds instClosedIicTopology OrderTopology.to_orderClosedTopology Set.pi_univ_Ici
pi_Ici_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ici Pi.preorder	—	pi_Ici_mem_nhds
pi_Ico_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ico Pi.preorder	—	Filter.mem_of_superset set_pi_mem_nhds Set.finite_univ Ico_mem_nhds OrderTopology.to_orderClosedTopology Set.pi_univ_Ico_subset
pi_Ico_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ico Pi.preorder	—	pi_Ico_mem_nhds
pi_Iic_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Iic Pi.preorder	—	set_pi_mem_nhds Set.toFinite Subtype.finite Iic_mem_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology Set.pi_univ_Iic
pi_Iic_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Iic Pi.preorder	—	pi_Iic_mem_nhds
pi_Iio_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Iio Pi.preorder	—	Filter.mem_of_superset set_pi_mem_nhds Set.finite_univ Iio_mem_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology Set.pi_univ_Iio_subset
pi_Iio_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Iio Pi.preorder	—	pi_Iio_mem_nhds
pi_Ioc_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioc Pi.preorder	—	Filter.mem_of_superset set_pi_mem_nhds Set.finite_univ Ioc_mem_nhds OrderTopology.to_orderClosedTopology Set.pi_univ_Ioc_subset
pi_Ioc_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioc Pi.preorder	—	pi_Ioc_mem_nhds
pi_Ioi_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioi Pi.preorder	—	pi_Iio_mem_nhds instOrderTopologyOrderDual
pi_Ioi_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioi Pi.preorder	—	pi_Ioi_mem_nhds
pi_Ioo_mem_nhds 📖	mathematical	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioo Pi.preorder	—	Filter.mem_of_superset set_pi_mem_nhds Set.finite_univ Ioo_mem_nhds OrderTopology.to_orderClosedTopology Set.pi_univ_Ioo_subset
pi_Ioo_mem_nhds' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhds Pi.topologicalSpace Set.Ioo Pi.preorder	—	pi_Ioo_mem_nhds
tendstoIccClassNhds 📖	mathematical	—	Filter.TendstoIxxClass Set.Icc nhds	—	nhds_eq_order iInf_subtype' Filter.HasBasis.tendstoIxxClass Filter.HasBasis.inf Filter.hasBasis_iInf_principal_finite Set.OrdConnected.out Set.OrdConnected.inter Set.ordConnected_biInter Set.ordConnected_Ioi Set.ordConnected_Iio
tendstoIccClassNhdsPi 📖	mathematical	OrderTopology	Filter.TendstoIxxClass Set.Icc Pi.preorder nhds Pi.topologicalSpace	—	nhds_pi Filter.pi.eq_1 Filter.smallSets_iInf Filter.smallSets_comap_eq_comap_image Continuous.tendsto continuous_apply Filter.Tendsto.smallSets_mono Filter.Tendsto.Icc tendstoIccClassNhds Filter.Tendsto.comp Filter.tendsto_fst Filter.tendsto_snd Filter.univ_mem' Set.image_subset_iff
tendstoIcoClassNhds 📖	mathematical	—	Filter.TendstoIxxClass Set.Ico nhds	—	Filter.tendstoIxxClass_of_subset Set.Ico_subset_Icc_self tendstoIccClassNhds
tendstoIocClassNhds 📖	mathematical	—	Filter.TendstoIxxClass Set.Ioc nhds	—	Filter.tendstoIxxClass_of_subset Set.Ioc_subset_Icc_self tendstoIccClassNhds
tendstoIooClassNhds 📖	mathematical	—	Filter.TendstoIxxClass Set.Ioo nhds	—	Filter.tendstoIxxClass_of_subset Set.Ioo_subset_Icc_self tendstoIccClassNhds
tendstoIxxNhdsWithin 📖	mathematical	—	Filter.TendstoIxxClass nhdsWithin	—	Filter.tendstoIxxClass_inf
tendsto_nhds_bot_mono 📖	—	Filter.Tendsto nhds Bot.bot OrderBot.toBot Preorder.toLE Filter.EventuallyLE	—	—	tendsto_nhds_top_mono instOrderTopologyOrderDual
tendsto_nhds_bot_mono' 📖	—	Filter.Tendsto nhds Bot.bot OrderBot.toBot Preorder.toLE Pi.hasLe	—	—	tendsto_nhds_bot_mono Filter.Eventually.of_forall
tendsto_nhds_top_mono 📖	—	Filter.Tendsto nhds Top.top OrderTop.toTop Preorder.toLE Filter.EventuallyLE	—	—	nhds_top_order Filter.mp_mem Filter.univ_mem' lt_of_lt_of_le
tendsto_nhds_top_mono' 📖	—	Filter.Tendsto nhds Top.top OrderTop.toTop Preorder.toLE Pi.hasLe	—	—	tendsto_nhds_top_mono Filter.Eventually.of_forall
tendsto_of_tendsto_of_tendsto_of_le_of_le 📖	—	Filter.Tendsto nhds Pi.hasLe Preorder.toLE	—	—	tendsto_of_tendsto_of_tendsto_of_le_of_le' Filter.Eventually.of_forall
tendsto_of_tendsto_of_tendsto_of_le_of_le' 📖	—	Filter.Tendsto nhds Filter.Eventually Preorder.toLE	—	—	Filter.Tendsto.of_smallSets Filter.Tendsto.Icc tendstoIccClassNhds Filter.Eventually.and
tendsto_order 📖	mathematical	—	Filter.Tendsto nhds Filter.Eventually Preorder.toLT	—	nhds_eq_order
tendsto_order_unbounded 📖	mathematical	Preorder.toLT Filter.Eventually	Filter.Tendsto nhds	—	nhds_order_unbounded

---

← Back to Index