DenselyOrdered

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

Statistics

Metric	Count
Definitions DenselyOrdered	1
Theorems exists_countable_dense_subset_no_bot_top, subsingleton_of_discreteTopology, Icc_mem_nhds_iff, Ico_mem_nhds_iff, Ico_subset_closure_interior, Ioc_mem_nhds_iff, Ioc_subset_closure_interior, closure_Ico, closure_Iio, closure_Iio', closure_Ioc, closure_Ioi, closure_Ioi', closure_Ioo, closure_interior_Icc, closure_uIoc, closure_uIoo, exists_countable_dense_no_bot_top, frontier_Icc, frontier_Ici, frontier_Ici', frontier_Ico, frontier_Iic, frontier_Iic', frontier_Iio, frontier_Iio', frontier_Ioc, frontier_Ioi, frontier_Ioi', frontier_Ioo, instNeBotNhdsWithinComplSetSingletonOfNontrivial, interior_Icc, interior_Ici, interior_Ici', interior_Ico, interior_Iic, interior_Iic', interior_Ioc, isClosed_Ico_iff, isClosed_Ioc_iff, isClosed_Ioo_iff, left_nhdsWithin_Ioc_neBot, left_nhdsWithin_Ioo_neBot, nhdsGT_neBot, nhdsGT_neBot_of_exists_gt, nhdsLT_neBot, nhdsLT_neBot_of_exists_lt, nhdsWithin_Iio_neBot, nhdsWithin_Iio_neBot', nhdsWithin_Iio_self_neBot', nhdsWithin_Ioi_neBot, nhdsWithin_Ioi_neBot', right_nhdsWithin_Ico_neBot, right_nhdsWithin_Ioo_neBot	54
Total	55

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_dense_subset_no_bot_top 📖	mathematical	Dense	Set Set.instHasSubset Set.Countable Set.instMembership	—	exists_countable_dense_subset HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset Set.Countable.mono diff_finite T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology instNeBotNhdsWithinComplSetSingletonOfNontrivial Set.Finite.union Set.Subsingleton.finite Set.subsingleton_isBot Set.subsingleton_isTop

DenselyOrdered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingleton_of_discreteTopology 📖	—	—	—	—	IsClosed.closure_eq isClosed_discrete closure_Ioo LT.lt.ne le_antisymm

(root)

Definitions

Name	Category	Theorems
DenselyOrdered 📖	CompData	57 math math: WithTop.denselyOrdered, instDenselyOrderedMultiplicative, FirstOrder.Language.realize_denselyOrdered_iff, Sum.denselyOrdered, Prod.Lex.instDenselyOrderedLex, OrderDual.denselyOrdered, NormedField.denselyOrdered_range_norm, Nonneg.instDenselyOrdered, denselyOrdered_units_iff, instDenselyOrderedProd, Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, StrictMono.denselyOrdered_range, instDenselyOrderedWithZeroOfNoMinOrder, Set.instDenselyOrdered, LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered, Sum.Lex.denselyOrdered_of_noMaxOrder, ENNReal.instDenselyOrdered, denselyOrdered_iff_of_orderIsoClass, instDenselyOrderedAdditive, Sum.Lex.denselyOrdered_of_noMinOrder, Irrational.instDenselyOrderedSubtypeReal, WithZero.denselyOrdered_set_iff_subsingleton, WithTop.denselyOrdered_iff, denselyOrdered_orderDual, denselyOrdered_iff_forall_not_covBy, denselyOrdered_multiplicative_iff, WithBot.denselyOrdered, LinearOrderedAddCommGroup.discrete_or_denselyOrdered, WithBot.denselyOrdered_iff, Subsingleton.instDenselyOrdered, denselyOrdered_additive_iff, Sum.denselyOrdered_iff, LocallyFiniteOrder.denselyOrdered_iff_subsingleton, WithTop.denselyOrdered_set_iff_subsingleton, FirstOrder.Language.denselyOrdered_of_dlo, PUnit.instDenselyOrdered, LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered, denselyOrdered_set_iff_subsingleton, Int.not_denselyOrdered, NormedField.denselyOrdered_range_nnnorm, denselyOrdered_iff_of_strictAnti, WithZero.denselyOrdered_iff, not_denselyOrdered_withZero_int, WithBot.denselyOrdered_set_iff_subsingleton, NNReal.instDenselyOrdered, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered, LinearOrderedCommGroup.discrete_or_denselyOrdered, LinearOrderedCommGroup.discrete_iff_not_denselyOrdered, instDenselyOrderedEReal, denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, Set.Subsingleton.denselyOrdered, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange, LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered, LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered, instDenselyOrderedUnits, LinearOrderedSemiField.toDenselyOrdered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioo	—	interior_Icc mem_interior_iff_mem_nhds
Ico_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioo	—	interior_Ico mem_interior_iff_mem_nhds
Ico_subset_closure_interior 📖	mathematical	—	Set Set.instHasSubset Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder closure interior	—	Set.Ioc_toDual Ioc_subset_closure_interior instOrderTopologyOrderDual OrderDual.denselyOrdered
Ioc_mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioo	—	interior_Ioc mem_interior_iff_mem_nhds
Ioc_subset_closure_interior 📖	mathematical	—	Set Set.instHasSubset Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder closure interior	—	eq_or_ne Set.Ioc_eq_empty interior_empty IsClosed.closure_eq T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Set.instReflSubset Set.Ioc_subset_Icc_self closure_Ioo closure_mono interior_maximal Set.Ioo_subset_Ioc_self isOpen_Ioo
closure_Ico 📖	mathematical	—	closure Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Icc	—	Set.Subset.antisymm closure_minimal Set.Ico_subset_Icc_self isClosed_Icc OrderTopology.to_orderClosedTopology Set.Subset.trans closure_Ioo subset_refl Set.instReflSubset closure_mono Set.Ioo_subset_Ico_self
closure_Iio 📖	mathematical	—	closure Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic	—	closure_Iio' Set.nonempty_Iio
closure_Iio' 📖	mathematical	Set.Nonempty Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	closure Set.Iic	—	closure_Ioi' instOrderTopologyOrderDual OrderDual.denselyOrdered
closure_Ioc 📖	mathematical	—	closure Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Icc	—	Set.Subset.antisymm closure_minimal Set.Ioc_subset_Icc_self isClosed_Icc OrderTopology.to_orderClosedTopology Set.Subset.trans closure_Ioo subset_refl Set.instReflSubset closure_mono Set.Ioo_subset_Ioc_self
closure_Ioi 📖	mathematical	—	closure Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ici	—	closure_Ioi' Set.nonempty_Ioi
closure_Ioi' 📖	mathematical	Set.Nonempty Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	closure Set.Ici	—	Set.Subset.antisymm closure_minimal Set.Ioi_subset_Ici_self isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology diff_subset_closure_iff Set.Ici_diff_Ioi_same Set.singleton_subset_iff IsGLB.mem_closure isGLB_Ioi
closure_Ioo 📖	mathematical	—	closure Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Icc	—	Set.Subset.antisymm closure_minimal Set.Ioo_subset_Icc_self isClosed_Icc OrderTopology.to_orderClosedTopology Ne.lt_or_gt diff_subset_closure_iff Set.Icc_diff_Ioo_same LT.lt.le Set.nonempty_Ioo IsGLB.mem_closure isGLB_Ioo IsLUB.mem_closure isLUB_Ioo Set.Icc_eq_empty_of_lt Set.empty_subset
closure_interior_Icc 📖	mathematical	—	closure interior Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	HasSubset.Subset.antisymm Set.instAntisymmSubset closure_minimal interior_subset isClosed_Icc OrderTopology.to_orderClosedTopology closure_Ioo closure_mono interior_maximal Set.Ioo_subset_Icc_self isOpen_Ioo
closure_uIoc 📖	mathematical	—	closure Set.uIoc Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	closure_Ioc
closure_uIoo 📖	mathematical	—	closure Set.uIoo Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	closure_Ioo
exists_countable_dense_no_bot_top 📖	mathematical	—	Set.Countable Dense Set Set.instMembership	—	Dense.exists_countable_dense_subset_no_bot_top separableSpace_univ dense_univ
frontier_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Icc Set Set.instInsert Set.instSingletonSet	—	closure_Icc OrderTopology.to_orderClosedTopology interior_Icc Set.Icc_diff_Ioo_same
frontier_Ici 📖	mathematical	—	frontier Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet	—	frontier_Ici' Set.nonempty_Iio
frontier_Ici' 📖	mathematical	Set.Nonempty Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Ici Set Set.instSingletonSet	—	closure_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology interior_Ici' Set.Ici_diff_Ioi_same
frontier_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Ico Set Set.instInsert Set.instSingletonSet	—	frontier.eq_1 closure_Ico LT.lt.ne interior_Ico Set.Icc_diff_Ioo_same LT.lt.le
frontier_Iic 📖	mathematical	—	frontier Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet	—	frontier_Iic' Set.nonempty_Ioi
frontier_Iic' 📖	mathematical	Set.Nonempty Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Iic Set Set.instSingletonSet	—	closure_Iic instClosedIicTopology OrderTopology.to_orderClosedTopology interior_Iic' Set.Iic_diff_Iio_same
frontier_Iio 📖	mathematical	—	frontier Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet	—	frontier_Iio' Set.nonempty_Iio
frontier_Iio' 📖	mathematical	Set.Nonempty Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set Set.instSingletonSet	—	closure_Iio' interior_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology Set.Iic_diff_Iio_same
frontier_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Ioc Set Set.instInsert Set.instSingletonSet	—	frontier.eq_1 closure_Ioc LT.lt.ne interior_Ioc Set.Icc_diff_Ioo_same LT.lt.le
frontier_Ioi 📖	mathematical	—	frontier Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet	—	frontier_Ioi' Set.nonempty_Ioi
frontier_Ioi' 📖	mathematical	Set.Nonempty Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set Set.instSingletonSet	—	closure_Ioi' interior_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology Set.Ici_diff_Ioi_same
frontier_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	frontier Set.Ioo Set Set.instInsert Set.instSingletonSet	—	frontier.eq_1 closure_Ioo LT.lt.ne interior_Ioo OrderTopology.to_orderClosedTopology Set.Icc_diff_Ioo_same LT.lt.le
instNeBotNhdsWithinComplSetSingletonOfNontrivial 📖	mathematical	—	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.forall_mem_nonempty_iff_neBot mem_nhdsWithin IsOpen.exists_Ioo_subset exists_between ne_or_eq LT.lt.trans LT.lt.ne
interior_Icc 📖	mathematical	—	interior Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioo	—	Set.Ici_inter_Iic interior_inter interior_Ici interior_Iic Set.Ioi_inter_Iio
interior_Ici 📖	mathematical	—	interior Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioi	—	interior_Ici' Set.nonempty_Iio
interior_Ici' 📖	mathematical	Set.Nonempty Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	interior Set.Ici Set.Ioi	—	Set.compl_Iio interior_compl closure_Iio' Set.compl_Iic
interior_Ico 📖	mathematical	—	interior Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioo	—	Set.Ici_inter_Iio interior_inter interior_Ici interior_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology Set.Ioi_inter_Iio
interior_Iic 📖	mathematical	—	interior Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iio	—	interior_Iic' Set.nonempty_Ioi
interior_Iic' 📖	mathematical	Set.Nonempty Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	interior Set.Iic Set.Iio	—	interior_Ici' instOrderTopologyOrderDual OrderDual.denselyOrdered
interior_Ioc 📖	mathematical	—	interior Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioo	—	Set.Ioi_inter_Iic interior_inter interior_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology interior_Iic Set.Ioi_inter_Iio
isClosed_Ico_iff 📖	mathematical	—	IsClosed Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	le_of_not_gt IsClosed.closure_eq Set.Icc_eq_Ico_same_iff closure_Ico LT.lt.ne LT.lt.le Set.Ico_eq_empty T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology
isClosed_Ioc_iff 📖	mathematical	—	IsClosed Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	le_of_not_gt IsClosed.closure_eq Set.Icc_eq_Ioc_same_iff closure_Ioc LT.lt.ne LT.lt.le Set.Ioc_eq_empty T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology
isClosed_Ioo_iff 📖	mathematical	—	IsClosed Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	le_of_not_gt IsClosed.closure_eq Set.Icc_eq_Ioo_same_iff closure_Ioo LT.lt.ne LT.lt.le Set.Ioo_eq_empty T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology
left_nhdsWithin_Ioc_neBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ioc	—	IsGLB.nhdsWithin_neBot isGLB_Ioc Set.nonempty_Ioc
left_nhdsWithin_Ioo_neBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ioo	—	IsGLB.nhdsWithin_neBot isGLB_Ioo Set.nonempty_Ioo
nhdsGT_neBot 📖	mathematical	—	Filter.NeBot nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nhdsWithin_Ioi_neBot le_rfl
nhdsGT_neBot_of_exists_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ioi	—	nhdsWithin_Ioi_neBot' le_refl
nhdsLT_neBot 📖	mathematical	—	Filter.NeBot nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nhdsWithin_Iio_neBot le_refl
nhdsLT_neBot_of_exists_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Iio	—	nhdsWithin_Iio_neBot' le_refl
nhdsWithin_Iio_neBot 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Iio	—	nhdsWithin_Iio_neBot' Set.nonempty_Iio
nhdsWithin_Iio_neBot' 📖	mathematical	Set.Nonempty Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Filter.NeBot nhdsWithin	—	mem_closure_iff_nhdsWithin_neBot closure_Iio'
nhdsWithin_Iio_self_neBot' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Iio	—	nhdsLT_neBot_of_exists_lt
nhdsWithin_Ioi_neBot 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ioi	—	nhdsWithin_Ioi_neBot' Set.nonempty_Ioi
nhdsWithin_Ioi_neBot' 📖	mathematical	Set.Nonempty Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Filter.NeBot nhdsWithin	—	mem_closure_iff_nhdsWithin_neBot closure_Ioi'
right_nhdsWithin_Ico_neBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ico	—	IsLUB.nhdsWithin_neBot isLUB_Ico Set.nonempty_Ico
right_nhdsWithin_Ioo_neBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.NeBot nhdsWithin Set.Ioo	—	IsLUB.nhdsWithin_neBot isLUB_Ioo Set.nonempty_Ioo

---

← Back to Index