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	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_atTop OrderDual.isOrderedAddMonoid AddCommGroup.add_comm instOrderTopologyOrderDual
add_atTop 📖	mathematical	Filter.Tendsto nhds Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	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	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_comm add_atBot
atBot_mul' 📖	mathematical	Filter.Tendsto Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_comm mul_atBot'
atTop_add 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	add_comm add_atTop
atTop_mul' 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_comm mul_atTop'
mul_atBot' 📖	mathematical	Filter.Tendsto nhds Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	mul_atTop' OrderDual.isOrderedMonoid CommGroup.mul_comm instOrderTopologyOrderDual
mul_atTop' 📖	mathematical	Filter.Tendsto nhds Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup	—	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	Filter Filter.instMembership nhdsWithin Set.Ici	—	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	Filter Filter.instMembership nhdsWithin Set.Ioi	—	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	Filter Filter.instMembership nhdsWithin Set.Iic	—	mem_nhdsGE instClosedIciTopologyOrderDual dual
mem_nhdsLT 📖	mathematical	Set Set.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter Filter.instMembership nhdsWithin Set.Iio	—	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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul 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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd 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 RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul 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.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 AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd 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.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 AddRightCancelSemigroup.toIsRightCancelAdd sub_lt_sub_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd 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 RightCancelSemigroup.toIsRightCancelMul IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul 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	—	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	—	TopologicalSpace.ext_nhds nhds_eq_iInf_mabs_div

---

← Back to Index