LeftRightNhds

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

Statistics

Metric	Count
Definitions	0
Theorems add_atBot, add_atTop, atBot_add, atBot_mul', atTop_add, atTop_mul', mul_atBot', mul_atTop', tendsto_nhds, tendsto_nhds, mem_nhdsGE, mem_nhdsGT, mem_nhdsLE, mem_nhdsLT, TFAE_mem_nhdsGE, TFAE_mem_nhdsGT, TFAE_mem_nhdsLE, TFAE_mem_nhdsLT, countable_setOf_isolated_left, countable_setOf_isolated_left_within, countable_setOf_isolated_right, countable_setOf_isolated_right_within, eventually_abs_sub_lt, eventually_mabs_div_lt, mem_nhdsGE_iff_exists_Icc_subset, mem_nhdsGE_iff_exists_Ico_subset, mem_nhdsGE_iff_exists_Ico_subset', mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset, mem_nhdsGT_iff_exists_Ioc_subset, mem_nhdsGT_iff_exists_Ioo_subset, mem_nhdsGT_iff_exists_Ioo_subset', mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset, mem_nhdsLE_iff_exists_Icc_subset, mem_nhdsLE_iff_exists_Ioc_subset, mem_nhdsLE_iff_exists_Ioc_subset', mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset, mem_nhdsLT_iff_exists_Ico_subset, mem_nhdsLT_iff_exists_Ioo_subset, mem_nhdsLT_iff_exists_Ioo_subset', mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset, nhdsGE_basis_Icc, nhdsGE_basis_Ico, nhdsGT_basis, nhdsGT_basis_of_exists_gt, nhdsGT_eq_bot_iff, nhdsLE_basis_Icc, nhdsLT_basis, nhdsLT_basis_of_exists_lt, nhdsLT_eq_bot_iff, nhds_basis_Icc_one_lt, nhds_basis_Icc_pos, nhds_basis_Ioo_one_lt, nhds_basis_Ioo_one_lt_of_one_lt, nhds_basis_Ioo_pos, nhds_basis_Ioo_pos_of_pos, nhds_basis_abs_sub_lt, nhds_basis_mabs_div_lt, nhds_basis_one_mabs_lt, nhds_basis_zero_abs_lt, nhds_eq_iInf_abs_sub, nhds_eq_iInf_mabs_div, orderTopology_of_nhds_abs, orderTopology_of_nhds_mabs	63
Total	63

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_atBot 📖	mathematical	Filter.Tendsto nhds Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_atTop OrderDual.isOrderedAddMonoid instOrderTopologyOrderDual
add_atTop 📖	mathematical	Filter.Tendsto nhds Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Filter.Subsingleton.atTop_eq Filter.tendsto_top NoMinOrder.exists_lt LinearOrderedAddCommGroup.to_noMinOrder Filter.tendsto_atTop_add_left_of_le' Filter.Eventually.mono eventually lt_mem_nhds le_of_lt
atBot_add 📖	mathematical	Filter.Tendsto Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	Filter.Tendsto AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_comm add_atBot
atBot_mul' 📖	mathematical	Filter.Tendsto Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	Filter.Tendsto MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mul_comm mul_atBot'
atTop_add 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	Filter.Tendsto AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_comm add_atTop
atTop_mul' 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	Filter.Tendsto MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mul_comm mul_atTop'
mul_atBot' 📖	mathematical	Filter.Tendsto nhds Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mul_atTop' OrderDual.isOrderedMonoid instOrderTopologyOrderDual
mul_atTop' 📖	mathematical	Filter.Tendsto nhds Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Filter.Subsingleton.atTop_eq NoMinOrder.exists_lt LinearOrderedCommGroup.to_noMinOrder Filter.tendsto_atTop_mul_left_of_le' Filter.Eventually.mono eventually lt_mem_nhds le_of_lt

LinearOrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_nhds 📖	mathematical	—	Filter.Tendsto nhds Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	nhds_eq_iInf_abs_sub iInf_congr_Prop abs_sub_comm Filter.tendsto_iInf Filter.tendsto_principal

LinearOrderedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_nhds 📖	mathematical	—	Filter.Tendsto nhds Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	nhds_eq_iInf_mabs_div iInf_congr_Prop mabs_div_comm

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_nhdsGE 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.mem_of_superset Icc_mem_nhdsGE out
mem_nhdsGT 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	nhdsWithin_mono Set.Ioi_subset_Ici_self mem_nhdsGE
mem_nhdsLE 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mem_nhdsGE instClosedIciTopologyOrderDual dual
mem_nhdsLT 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mem_nhdsGT instClosedIciTopologyOrderDual dual

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE_mem_nhdsGE 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	List.TFAE Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Icc Set.Ico Set.instMembership Set.Ioc Set.instHasSubset Set.Ioi	—	nhdsWithin_Icc_eq_nhdsGE instClosedIciTopology OrderTopology.to_orderClosedTopology nhdsWithin_Ico_eq_nhdsGE Filter.HasBasis.mem_iff nhdsGE_basis_of_exists_gt lt_min min_le_right HasSubset.Subset.trans Set.instIsTransSubset Set.Ico_subset_Ico_right min_le_left List.tfae_of_cycle
TFAE_mem_nhdsGT 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	List.TFAE Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioc Set.Ioo Set.instMembership Set.instHasSubset	—	nhdsWithin_Ioc_eq_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology nhdsWithin_Ioo_eq_nhdsGT Filter.mem_of_superset Ioo_mem_nhdsGT mem_nhdsWithin_iff_exists_mem_nhds_inter exists_Ico_subset_of_mem_nhds' le_of_lt List.tfae_of_cycle
TFAE_mem_nhdsLE 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	List.TFAE Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Icc Set.Ioc Set.instMembership Set.Ico Set.instHasSubset Set.Iio	—	Set.Icc_toDual Set.Ico_toDual Set.Ioc_toDual EquivLike.range_eq_univ TFAE_mem_nhdsGE instOrderTopologyOrderDual LT.lt.dual
TFAE_mem_nhdsLT 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	List.TFAE Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ico Set.Ioo Set.instMembership Set.instHasSubset	—	Set.Ioc_toDual Set.Ioo_toDual EquivLike.range_eq_univ TFAE_mem_nhdsGT instOrderTopologyOrderDual LT.lt.dual
countable_setOf_isolated_left 📖	mathematical	—	Set.Countable setOf Filter nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter.instBot	—	countable_setOf_isolated_right instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_setOf_isolated_left_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Filter nhdsWithin Set.instInter Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter.instBot	—	countable_setOf_isolated_right_within instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
countable_setOf_isolated_right 📖	mathematical	—	Set.Countable setOf Filter nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter.instBot	—	Set.Countable.union Set.Subsingleton.countable Set.subsingleton_isTop countable_setOf_covBy_right
countable_setOf_isolated_right_within 📖	mathematical	—	Set.Countable setOf Set Set.instMembership Filter nhdsWithin Set.instInter Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter.instBot	—	exists_Ico_subset_of_mem_nhds Mathlib.Tactic.Contrapose.contrapose₁ Set.Nonempty.mono LT.lt.le Set.PairwiseDisjoint.countable_of_Ioo Set.disjoint_iff_forall_ne LT.lt.ne LT.lt.trans LT.lt.trans_le lt_of_le_of_ne Disjoint.symm Function.sometimes_spec Set.Countable.mono Set.Subsingleton.countable Set.subsingleton_isTop
eventually_abs_sub_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid nhds	—	Filter.mem_iInf_of_mem abs_sub_comm Filter.mem_principal_self nhds_eq_iInf_abs_sub
eventually_mabs_div_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid nhds	—	Filter.mem_iInf_of_mem mabs_div_comm nhds_eq_iInf_mabs_div
mem_nhdsGE_iff_exists_Icc_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.instHasSubset Set.Icc	—	Filter.HasBasis.mem_iff nhdsGE_basis_Icc
mem_nhdsGE_iff_exists_Ico_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioi Set.instHasSubset Set.Ico	—	NoMaxOrder.exists_gt mem_nhdsGE_iff_exists_Ico_subset'
mem_nhdsGE_iff_exists_Ico_subset' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioi Set.instHasSubset Set.Ico	—	List.TFAE.out TFAE_mem_nhdsGE zero_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat
mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioc Set.instHasSubset Set.Ico	—	List.TFAE.out TFAE_mem_nhdsGE zero_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat
mem_nhdsGT_iff_exists_Ioc_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ioc	—	mem_nhdsGT_iff_exists_Ioo_subset exists_between lt_of_le_of_lt Set.Subset.trans Set.Ioo_subset_Ioc_self
mem_nhdsGT_iff_exists_Ioo_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ioo	—	NoMaxOrder.exists_gt mem_nhdsGT_iff_exists_Ioo_subset'
mem_nhdsGT_iff_exists_Ioo_subset' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ioo	—	List.TFAE.out TFAE_mem_nhdsGT
mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ioc Set.instHasSubset Set.Ioo	—	List.TFAE.out TFAE_mem_nhdsGT
mem_nhdsLE_iff_exists_Icc_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.instHasSubset Set.Icc	—	mem_nhdsGE_iff_exists_Icc_subset instOrderTopologyOrderDual OrderDual.noMaxOrder OrderDual.denselyOrdered Set.Icc_toDual EquivLike.range_eq_univ
mem_nhdsLE_iff_exists_Ioc_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Iio Set.instHasSubset Set.Ioc	—	NoMinOrder.exists_lt mem_nhdsLE_iff_exists_Ioc_subset'
mem_nhdsLE_iff_exists_Ioc_subset' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Iio Set.instHasSubset Set.Ioc	—	List.TFAE.out TFAE_mem_nhdsLE zero_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat
mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ico Set.instHasSubset Set.Ioc	—	List.TFAE.out TFAE_mem_nhdsLE zero_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat
mem_nhdsLT_iff_exists_Ico_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ico	—	mem_nhdsGT_iff_exists_Ioc_subset instOrderTopologyOrderDual OrderDual.noMaxOrder OrderDual.denselyOrdered Set.Ioc_toDual EquivLike.range_eq_univ
mem_nhdsLT_iff_exists_Ioo_subset 📖	mathematical	—	Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ioo	—	NoMinOrder.exists_lt mem_nhdsLT_iff_exists_Ioo_subset'
mem_nhdsLT_iff_exists_Ioo_subset' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.instHasSubset Set.Ioo	—	List.TFAE.out TFAE_mem_nhdsLT
mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Filter Filter.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instMembership Set.Ico Set.instHasSubset Set.Ioo	—	List.TFAE.out TFAE_mem_nhdsLT
nhdsGE_basis_Icc 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Icc	—	Filter.HasBasis.to_hasBasis nhdsGE_basis Set.Icc_subset_Ico_right exists_between Set.Ico_subset_Icc_self
nhdsGE_basis_Ico 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ico	—	mem_nhdsGE_iff_exists_Ico_subset
nhdsGT_basis 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo	—	nhdsGT_basis_of_exists_gt NoMaxOrder.exists_gt
nhdsGT_basis_of_exists_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo	—	mem_nhdsGT_iff_exists_Ioo_subset'
nhdsGT_eq_bot_iff 📖	mathematical	—	nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter Filter.instBot IsTop Preorder.toLE CovBy Preorder.toLT	—	IsMax.Ioi_eq IsTop.isMax nhdsWithin_empty Filter.HasBasis.eq_bot_iff nhdsGT_basis_of_exists_gt not_isMax_iff isTop_iff_isMax SemilatticeSup.instIsDirectedOrder
nhdsLE_basis_Icc 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Icc	—	mem_nhdsLE_iff_exists_Icc_subset
nhdsLT_basis 📖	mathematical	—	Filter.HasBasis nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo	—	nhdsLT_basis_of_exists_lt NoMinOrder.exists_lt
nhdsLT_basis_of_exists_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.HasBasis nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo	—	mem_nhdsLT_iff_exists_Ioo_subset'
nhdsLT_eq_bot_iff 📖	mathematical	—	nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot Filter Filter.instBot IsBot Preorder.toLE CovBy Preorder.toLT	—	ofDual_covBy_ofDual_iff nhdsGT_eq_bot_iff instOrderTopologyOrderDual
nhds_basis_Icc_one_lt 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Set.Icc DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	Filter.HasBasis.to_hasBasis nhds_basis_Ioo_one_lt exists_between Set.Icc_subset_Ioo div_lt_div_left' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_mul_of_covariant_mul mul_lt_mul_right Set.Ioo_subset_Icc_self
nhds_basis_Icc_pos 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.Icc SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	Filter.HasBasis.to_hasBasis nhds_basis_Ioo_pos exists_between Set.Icc_subset_Ioo sub_lt_sub_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add add_lt_add_right Set.Ioo_subset_Icc_self
nhds_basis_Ioo_one_lt 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Set.Ioo DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid contravariant_lt_of_covariant_le IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono nhds_basis_mabs_div_lt
nhds_basis_Ioo_one_lt_of_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Preorder.toLE Set.Ioo DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	Filter.HasBasis.restrict nhds_basis_Ioo_one_lt lt_min min_le_left Set.Ioo_subset_Ioo div_le_div_left' IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul min_le_right mul_le_mul_right
nhds_basis_Ioo_pos 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.Ioo SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono abs_lt neg_lt_sub_iff_lt_add nhds_basis_abs_sub_lt
nhds_basis_Ioo_pos_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLE Set.Ioo SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	Filter.HasBasis.restrict nhds_basis_Ioo_pos lt_min min_le_left Set.Ioo_subset_Ioo sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add min_le_right add_le_add_right
nhds_basis_abs_sub_lt 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid setOf abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	nhds_eq_iInf_abs_sub iInf_congr_Prop abs_sub_comm Filter.hasBasis_biInf_principal' lt_min LT.lt.trans_le min_le_left min_le_right NoMaxOrder.exists_gt
nhds_basis_mabs_div_lt 📖	mathematical	—	Filter.HasBasis nhds Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid setOf mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	nhds_eq_iInf_mabs_div iInf_congr_Prop mabs_div_comm Filter.hasBasis_biInf_principal' lt_min LT.lt.trans_le min_le_left min_le_right NoMaxOrder.exists_gt
nhds_basis_one_mabs_lt 📖	mathematical	—	Filter.HasBasis nhds InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf mabs CommGroup.toGroup	—	div_one nhds_basis_mabs_div_lt
nhds_basis_zero_abs_lt 📖	mathematical	—	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf abs AddCommGroup.toAddGroup	—	sub_zero nhds_basis_abs_sub_lt
nhds_eq_iInf_abs_sub 📖	mathematical	—	nhds iInf Filter Filter.instInfSet Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.principal setOf abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	nhds_eq_order iInf_congr_Prop abs_lt IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add Filter.inf_principal iInf_inf_eq Equiv.iInf_congr sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le sub_lt_sub_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Set.mem_Iio neg_sub Set.mem_Ioi inf_comm
nhds_eq_iInf_mabs_div 📖	mathematical	—	nhds iInf Filter Filter.instInfSet Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Filter.principal setOf mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	nhds_eq_order iInf_congr_Prop IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul iInf_inf_eq Equiv.iInf_congr IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedMonoid.toIsOrderedCancelMonoid contravariant_lt_of_covariant_le IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono inv_div inf_comm
orderTopology_of_nhds_abs 📖	mathematical	nhds iInf Filter Filter.instInfSet Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.principal setOf abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	TopologicalSpace.ext_nhds nhds_eq_iInf_abs_sub
orderTopology_of_nhds_mabs 📖	mathematical	nhds iInf Filter Filter.instInfSet Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Filter.principal setOf mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	TopologicalSpace.ext_nhds nhds_eq_iInf_mabs_div

---

← Back to Index