NhdsWithin

📁 Source: Mathlib/Topology/NhdsWithin.lean

Statistics

Metric	Count
Definitions	0
Theorems `nhdsWithin_neBot`, `piMap`, `self_of_nhdsWithin`, `eq_of_nhdsWithin`, `mem_interior`, `mem_interior_iff`, `if_nhdsWithin`, `piecewise_nhdsWithin`, `mem_of_nhdsWithin_neBot`, `nhdsWithin_eq`, `instNeBotNhdsWithinIio`, `instNeBotNhdsWithinIoi`, `eventuallyEq_nhdsWithin`, `preimage_mem_nhdsWithin`, `map_nhdsSet_eq`, `closure_pi_set`, `continuousAt_iff_punctured_nhds`, `dense_pi`, `diff_mem_nhdsWithin_compl`, `diff_mem_nhdsWithin_diff`, `eventuallyEq_nhdsWithin_iff`, `eventuallyEq_nhdsWithin_of_eqOn`, `eventuallyEq_nhds_of_eventuallyEq_nhdsNE`, `eventually_eventually_nhdsWithin`, `eventually_mem_nhdsWithin`, `eventually_mem_nhdsWithin_iff`, `eventually_mem_of_tendsto_nhdsWithin`, `eventually_nhdsWithin_iff`, `eventually_nhdsWithin_of_eventually_nhds`, `eventually_nhdsWithin_of_forall`, `eventually_nhds_nhdsWithin`, `eventually_nhds_subtype_iff`, `frequently_nhdsWithin_iff`, `frequently_nhds_subtype_iff`, `insert_mem_nhdsWithin_insert`, `insert_mem_nhds_iff`, `instNeBotNhdsWithinUnivPi`, `inter_mem_nhdsWithin`, `inter_mem_nhdsWithin_inter`, `map_nhdsSet_induced_eq`, `map_nhdsSet_subtype_val`, `map_nhdsWithin`, `mem_closure_ne_iff_frequently_within`, `mem_closure_pi`, `mem_nhdsSet`, `mem_nhdsSetWithin`, `mem_nhdsSet_induced`, `mem_nhdsSet_subtype_iff_nhdsSetWithin`, `mem_nhdsWithin`, `mem_nhdsWithin_iff_eventually`, `mem_nhdsWithin_iff_eventuallyEq`, `mem_nhdsWithin_iff_exists_mem_nhds_inter`, `mem_nhdsWithin_insert`, `mem_nhdsWithin_inter_self`, `mem_nhdsWithin_of_mem_nhds`, `mem_nhdsWithin_self_inter`, `mem_nhdsWithin_subtype`, `mem_nhds_subtype_iff_nhdsWithin`, `mem_of_mem_nhdsWithin`, `nhdsNE_sup_pure`, `nhdsSetWithin_basis_open`, `nhdsSetWithin_empty`, `nhdsSetWithin_empty'`, `nhdsSetWithin_eq_principal_of_subset`, `nhdsSetWithin_hasBasis`, `nhdsSetWithin_mono_left`, `nhdsSetWithin_mono_right`, `nhdsSetWithin_prod_le`, `nhdsSetWithin_self`, `nhdsSetWithin_singleton`, `nhdsSetWithin_univ`, `nhdsSetWithin_univ'`, `nhdsSet_induced`, `nhdsWithin_basis_open`, `nhdsWithin_biUnion`, `nhdsWithin_empty`, `nhdsWithin_eq`, `nhdsWithin_eq_iff_eventuallyEq`, `nhdsWithin_eq_map_subtype_coe`, `nhdsWithin_eq_nhds`, `nhdsWithin_eq_nhdsWithin`, `nhdsWithin_eq_nhdsWithin'`, `nhdsWithin_hasBasis`, `nhdsWithin_iUnion`, `nhdsWithin_insert`, `nhdsWithin_inter`, `nhdsWithin_inter'`, `nhdsWithin_inter_of_mem`, `nhdsWithin_inter_of_mem'`, `nhdsWithin_le_iff`, `nhdsWithin_le_nhds`, `nhdsWithin_le_of_mem`, `nhdsWithin_neBot_of_mem`, `nhdsWithin_pi_eq`, `nhdsWithin_pi_eq'`, `nhdsWithin_pi_eq_bot`, `nhdsWithin_pi_neBot`, `nhdsWithin_pi_univ_eq`, `nhdsWithin_prod`, `nhdsWithin_restrict`, `nhdsWithin_restrict'`, `nhdsWithin_restrict''`, `nhdsWithin_sUnion`, `nhdsWithin_singleton`, `nhdsWithin_subtype`, `nhdsWithin_union`, `nhdsWithin_univ`, `nhds_bind_nhdsWithin`, `nhds_eq_nhdsWithin_sup_nhdsWithin`, `nhds_of_Ici_Iic`, `nhds_of_nhdsWithin_of_nhds`, `preimage_coe_mem_nhds_subtype`, `preimage_nhdsWithin_coinduced'`, `preimage_nhds_within_coinduced`, `principal_inter_le_nhdsSetWithin`, `punctured_nhds_eq_nhdsWithin_sup_nhdsWithin`, `pure_le_nhdsWithin`, `pure_sup_nhdsNE`, `self_mem_nhdsWithin`, `tendsto_const_nhdsWithin`, `tendsto_nhdsWithin_congr`, `tendsto_nhdsWithin_iff`, `tendsto_nhdsWithin_iff_subtype`, `tendsto_nhdsWithin_mono_left`, `tendsto_nhdsWithin_mono_right`, `tendsto_nhdsWithin_of_tendsto_nhds`, `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`, `tendsto_nhdsWithin_range`, `tendsto_nhds_of_tendsto_nhdsWithin`, `union_mem_nhds_of_mem_nhdsWithin`	130
Total	130

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsWithin_neBot` 📖	mathematical	`DenseRange`	`Filter.NeBot` `nhdsWithin` `Set.range`	—	`mem_closure_iff_clusterPt`
`piMap` 📖	mathematical	`DenseRange`	`Pi.topologicalSpace` `Pi.map`	—	`eq_1` `Set.range_piMap` `dense_pi`

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`self_of_nhdsWithin` 📖	—	`Filter.Eventually` `nhdsWithin` `Set` `Set.instMembership`	—	—	`mem_of_mem_nhdsWithin`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_nhdsWithin` 📖	—	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	—	—	`Filter.Eventually.self_of_nhdsWithin`
`mem_interior` 📖	—	`Filter.EventuallyEq` `nhds` `Set` `Set.instMembership` `interior`	—	—	`nhdsWithin_eq_iff_eventuallyEq`
`mem_interior_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`Set` `Set.instMembership` `interior`	—	`mem_interior` `symm`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`if_nhdsWithin` 📖	—	`Filter.Tendsto` `nhdsWithin` `Set` `Set.instInter` `setOf`	—	—	`piecewise_nhdsWithin`
`piecewise_nhdsWithin` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `Set` `Set.instInter` `Compl.compl` `Set.instCompl`	`Set.piecewise`	—	`piecewise` `nhdsWithin_inter'`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_of_nhdsWithin_neBot` 📖	mathematical	—	`Set` `Set.instMembership`	—	`mem_closure_iff_nhdsWithin_neBot` `closure_eq`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsWithin_eq` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`nhdsWithin` `nhds`	—	`nhdsWithin_eq_nhds` `mem_nhds`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNeBotNhdsWithinIio` 📖	mathematical	`Filter.NeBot` `nhdsWithin` `Set.Iio`	`topologicalSpace` `preorder`	—	`instNeBotNhdsWithinUnivPi` `Filter.NeBot.mono` `nhdsWithin_mono` `lt_of_strongLT`
`instNeBotNhdsWithinIoi` 📖	mathematical	`Filter.NeBot` `nhdsWithin` `Set.Ioi`	`topologicalSpace` `preorder`	—	`instNeBotNhdsWithinIio` `OrderDual.instNeBotNhdsWithinIio`

Set.EqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_nhdsWithin` 📖	mathematical	`Set.EqOn`	`Filter.EventuallyEq` `nhdsWithin`	—	`eventuallyEq_nhdsWithin_of_eqOn`

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_mem_nhdsWithin` 📖	mathematical	`Set.MapsTo`	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.preimage`	—	`Filter.mem_of_superset` `self_mem_nhdsWithin`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_nhdsSet_eq` 📖	mathematical	`Topology.IsInducing`	`Filter.map` `nhdsSet` `nhdsSetWithin` `Set.image` `Set.range`	—	`map_nhdsSet_induced_eq` `eq_induced`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_pi_set` 📖	mathematical	—	`closure` `Pi.topologicalSpace` `Set.pi`	—	`Set.ext` `mem_closure_pi`
`continuousAt_iff_punctured_nhds` 📖	mathematical	—	`ContinuousAt` `Filter.Tendsto` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`pure_sup_nhdsNE`
`dense_pi` 📖	mathematical	`Dense`	`Pi.topologicalSpace` `Set.pi`	—	`closure_pi_set` `Set.pi_congr` `Dense.closure_eq` `Set.pi_univ`
`diff_mem_nhdsWithin_compl` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `Compl.compl` `Set.instCompl` `Set.instSDiff`	—	`Filter.diff_mem_inf_principal_compl`
`diff_mem_nhdsWithin_diff` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instSDiff`	—	`nhdsWithin.eq_1` `Set.diff_eq` `Filter.inf_principal` `inf_assoc` `Filter.inter_mem_inf` `Filter.mem_principal_self`
`eventuallyEq_nhdsWithin_iff` 📖	mathematical	—	`Filter.EventuallyEq` `nhdsWithin` `Filter.Eventually` `nhds`	—	`Filter.mem_inf_principal`
`eventuallyEq_nhdsWithin_of_eqOn` 📖	mathematical	`Set.EqOn`	`Filter.EventuallyEq` `nhdsWithin`	—	`Filter.mem_inf_of_right`
`eventuallyEq_nhds_of_eventuallyEq_nhdsNE` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`nhds`	—	`Filter.mp_mem` `eventually_nhdsWithin_iff` `Filter.univ_mem'`
`eventually_eventually_nhdsWithin` 📖	mathematical	—	`Filter.Eventually` `nhdsWithin`	—	`Filter.Eventually.mono` `Filter.Eventually.self_of_nhds` `Filter.Eventually.filter_mono` `inf_le_left` `eventually_nhds_nhdsWithin`
`eventually_mem_nhdsWithin` 📖	mathematical	—	`Filter.Eventually` `Set` `Set.instMembership` `nhdsWithin`	—	`self_mem_nhdsWithin`
`eventually_mem_nhdsWithin_iff` 📖	mathematical	—	`Filter.Eventually` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	`eventually_eventually_nhdsWithin`
`eventually_mem_of_tendsto_nhdsWithin` 📖	mathematical	`Filter.Tendsto` `nhdsWithin`	`Filter.Eventually` `Set` `Set.instMembership`	—	`nhdsWithin_eq` `Set.mem_univ` `isOpen_univ`
`eventually_nhdsWithin_iff` 📖	mathematical	—	`Filter.Eventually` `nhdsWithin` `nhds`	—	`Filter.eventually_inf_principal`
`eventually_nhdsWithin_of_eventually_nhds` 📖	mathematical	`Filter.Eventually` `nhds`	`nhdsWithin`	—	`mem_nhdsWithin_of_mem_nhds`
`eventually_nhdsWithin_of_forall` 📖	mathematical	—	`Filter.Eventually` `nhdsWithin`	—	`Filter.mem_inf_of_right`
`eventually_nhds_nhdsWithin` 📖	mathematical	—	`Filter.Eventually` `nhdsWithin` `nhds`	—	`Filter.ext_iff` `nhds_bind_nhdsWithin`
`eventually_nhds_subtype_iff` 📖	mathematical	—	`Filter.Eventually` `Set.Elem` `Set` `Set.instMembership` `nhds` `instTopologicalSpaceSubtype` `nhdsWithin`	—	`preimage_coe_mem_nhds_subtype`
`frequently_nhdsWithin_iff` 📖	mathematical	—	`Filter.Frequently` `nhdsWithin` `Set` `Set.instMembership` `nhds`	—	`Filter.frequently_inf_principal`
`frequently_nhds_subtype_iff` 📖	mathematical	—	`Filter.Frequently` `Set.Elem` `Set` `Set.instMembership` `nhds` `instTopologicalSpaceSubtype` `nhdsWithin`	—	`Iff.not` `eventually_nhds_subtype_iff`
`insert_mem_nhdsWithin_insert` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInsert`	—	`nhdsWithin_insert` `Filter.mem_of_superset`
`insert_mem_nhds_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instInsert` `nhdsWithin` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	—
`instNeBotNhdsWithinUnivPi` 📖	mathematical	`Filter.NeBot` `nhdsWithin`	`Pi.topologicalSpace` `Set.pi` `Set.univ`	—	—
`inter_mem_nhdsWithin` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `Set.instInter`	—	`Filter.inter_mem` `self_mem_nhdsWithin` `Filter.mem_inf_of_left`
`inter_mem_nhdsWithin_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`Filter.inter_mem` `nhdsWithin_mono` `Set.inter_subset_left` `Set.inter_subset_right`
`map_nhdsSet_induced_eq` 📖	mathematical	—	`Filter.map` `nhdsSet` `TopologicalSpace.induced` `nhdsSetWithin` `Set.image` `Set.range`	—	`nhdsSet_induced` `Filter.map_comap` `nhdsSetWithin.eq_1`
`map_nhdsSet_subtype_val` 📖	mathematical	—	`Filter.map` `Set.Elem` `Set` `Set.instMembership` `nhdsSet` `instTopologicalSpaceSubtype` `nhdsSetWithin` `Set.image`	—	`Topology.IsInducing.map_nhdsSet_eq` `Topology.IsInducing.subtypeVal` `Subtype.range_val`
`map_nhdsWithin` 📖	mathematical	—	`Filter.map` `nhdsWithin` `iInf` `Filter` `Set` `Filter.instInfSet` `Set.instMembership` `setOf` `IsOpen` `Filter.principal` `Set.image` `Set.instInter`	—	`Filter.HasBasis.eq_biInf` `Filter.HasBasis.map` `nhdsWithin_basis_open`
`mem_closure_ne_iff_frequently_within` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Set.instSDiff` `Set.instSingletonSet` `Filter.Frequently` `nhdsWithin` `Compl.compl` `Set.instCompl`	—	—
`mem_closure_pi` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Pi.topologicalSpace` `Set.pi`	—	—
`mem_nhdsSet` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `Set.instHasSubset` `IsOpen`	—	`Set.inter_univ`
`mem_nhdsSetWithin` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSetWithin` `IsOpen` `Set.instHasSubset` `Set.instInter`	—	`Filter.HasBasis.mem_iff` `nhdsSetWithin_basis_open`
`mem_nhdsSet_induced` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `TopologicalSpace.induced` `Set.image` `Set.instHasSubset` `Set.preimage`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_mono` `Set.instReflSubset` `subset_rfl` `Eq.trans_subset` `Set.image_subset_iff` `Set.preimage_mono`
`mem_nhdsSet_subtype_iff_nhdsSetWithin` 📖	mathematical	—	`Set` `Set.Elem` `Filter` `Filter.instMembership` `nhdsSet` `instTopologicalSpaceSubtype` `Set.instMembership` `nhdsSetWithin` `Set.image`	—	`map_nhdsSet_subtype_val` `Filter.image_mem_map_iff` `Subtype.val_injective`
`mem_nhdsWithin` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `IsOpen` `Set.instMembership` `Set.instHasSubset` `Set.instInter`	—	`Filter.HasBasis.mem_iff` `nhdsWithin_basis_open`
`mem_nhdsWithin_iff_eventually` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Filter.Eventually` `nhds`	—	`Filter.eventually_inf_principal`
`mem_nhdsWithin_iff_eventuallyEq` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Filter.EventuallyEq` `nhds` `Set.instInter`	—	—
`mem_nhdsWithin_iff_exists_mem_nhds_inter` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `nhds` `Set.instHasSubset` `Set.instInter`	—	`Filter.HasBasis.mem_iff` `nhdsWithin_hasBasis` `Filter.basis_sets`
`mem_nhdsWithin_insert` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.instInsert` `Set.instMembership`	—	`nhdsWithin_insert`
`mem_nhdsWithin_inter_self` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.instInter`	—	`mem_nhdsWithin_iff_eventuallyEq` `Set.inter_assoc` `Set.inter_self`
`mem_nhdsWithin_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin`	—	`Filter.mem_inf_of_left`
`mem_nhdsWithin_self_inter` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.instInter`	—	`mem_nhdsWithin_iff_eventuallyEq` `Set.inter_comm` `Set.inter_assoc` `Set.inter_self`
`mem_nhdsWithin_subtype` 📖	mathematical	—	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhdsWithin` `instTopologicalSpaceSubtype` `Filter.comap` `Set.image`	—	`nhdsWithin.eq_1` `nhds_subtype` `Filter.principal_subtype` `Filter.comap_inf`
`mem_nhds_subtype_iff_nhdsWithin` 📖	mathematical	—	`Set` `Set.Elem` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpaceSubtype` `Set.instMembership` `nhdsWithin` `Set.image`	—	`map_nhds_subtype_val` `Filter.image_mem_map_iff` `Subtype.val_injective`
`mem_of_mem_nhdsWithin` 📖	—	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhdsWithin`	—	—	`pure_le_nhdsWithin`
`nhdsNE_sup_pure` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.instPure` `nhds`	—	`nhdsWithin_singleton` `nhdsWithin_union` `Set.compl_union_self` `nhdsWithin_univ`
`nhdsSetWithin_basis_open` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhdsSetWithin` `IsOpen` `Set.instHasSubset` `Set.instInter`	—	`nhdsSetWithin_hasBasis` `hasBasis_nhdsSet`
`nhdsSetWithin_empty` 📖	mathematical	—	`nhdsSetWithin` `Set` `Set.instEmptyCollection` `Bot.bot` `Filter` `Filter.instBot`	—	`Filter.principal_empty` `inf_of_le_right`
`nhdsSetWithin_empty'` 📖	mathematical	—	`nhdsSetWithin` `Set` `Set.instEmptyCollection` `Bot.bot` `Filter` `Filter.instBot`	—	`nhdsSet_empty` `inf_of_le_left`
`nhdsSetWithin_eq_principal_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`nhdsSetWithin` `Filter.principal`	—	`inf_of_le_right` `LE.le.trans` `Filter.principal_mono` `principal_le_nhdsSet`
`nhdsSetWithin_hasBasis` 📖	mathematical	`Filter.HasBasis` `nhdsSet`	`nhdsSetWithin` `Set` `Set.instInter`	—	`Filter.HasBasis.inf_principal`
`nhdsSetWithin_mono_left` 📖	mathematical	`Set` `Set.instHasSubset`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSetWithin`	—	`inf_le_inf_right` `nhdsSet_mono`
`nhdsSetWithin_mono_right` 📖	mathematical	`Set` `Set.instHasSubset`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSetWithin`	—	`inf_le_inf_left` `Filter.principal_mono`
`nhdsSetWithin_prod_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSetWithin` `instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd` `Filter.instSProd`	—	`Filter.prod_principal_principal` `inf_le_of_left_le` `nhdsSet_prod_le`
`nhdsSetWithin_self` 📖	mathematical	—	`nhdsSetWithin` `Filter.principal`	—	`inf_of_le_right`
`nhdsSetWithin_singleton` 📖	mathematical	—	`nhdsSetWithin` `Set` `Set.instSingletonSet` `nhdsWithin`	—	`nhdsSet_singleton`
`nhdsSetWithin_univ` 📖	mathematical	—	`nhdsSetWithin` `Set.univ` `nhdsSet`	—	`Filter.principal_univ` `inf_of_le_left`
`nhdsSetWithin_univ'` 📖	mathematical	—	`nhdsSetWithin` `Set.univ` `Filter.principal`	—	`nhdsSet_univ` `inf_of_le_right`
`nhdsSet_induced` 📖	mathematical	—	`nhdsSet` `TopologicalSpace.induced` `Filter.comap` `Set.image`	—	`Filter.ext` `mem_nhdsSet_induced` `Filter.mem_comap`
`nhdsWithin_basis_open` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhdsWithin` `Set.instMembership` `IsOpen` `Set.instInter`	—	`nhdsWithin_hasBasis` `nhds_basis_opens`
`nhdsWithin_biUnion` 📖	mathematical	—	`nhdsWithin` `Set.iUnion` `Set` `Set.instMembership` `iSup` `Filter` `Filter.instSupSet`	—	`Set.Finite.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `nhdsWithin_empty` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `Set.biUnion_insert` `nhdsWithin_union` `iSup_insert`
`nhdsWithin_empty` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instEmptyCollection` `Bot.bot` `Filter` `Filter.instBot`	—	`nhdsWithin.eq_1` `Filter.principal_empty` `inf_bot_eq`
`nhdsWithin_eq` 📖	mathematical	—	`nhdsWithin` `iInf` `Filter` `Set` `Filter.instInfSet` `Set.instMembership` `setOf` `IsOpen` `Filter.principal` `Set.instInter`	—	`Filter.HasBasis.eq_biInf` `Filter.HasBasis.inf_principal` `nhds_basis_opens`
`nhdsWithin_eq_iff_eventuallyEq` 📖	mathematical	—	`nhdsWithin` `Filter.EventuallyEq` `nhds`	—	`Filter.set_eventuallyEq_iff_inf_principal`
`nhdsWithin_eq_map_subtype_coe` 📖	mathematical	`Set` `Set.instMembership`	`nhdsWithin` `Filter.map` `nhds` `instTopologicalSpaceSubtype`	—	`map_nhds_subtype_val`
`nhdsWithin_eq_nhds` 📖	mathematical	—	`nhdsWithin` `nhds` `Set` `Filter` `Filter.instMembership`	—	`inf_eq_left` `Filter.le_principal_iff`
`nhdsWithin_eq_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `IsOpen` `Set.instInter`	`nhdsWithin`	—	`nhdsWithin_restrict`
`nhdsWithin_eq_nhdsWithin'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instInter`	`nhdsWithin`	—	`nhdsWithin_restrict'`
`nhdsWithin_hasBasis` 📖	mathematical	`Filter.HasBasis` `nhds`	`nhdsWithin` `Set` `Set.instInter`	—	`Filter.HasBasis.inf_principal`
`nhdsWithin_iUnion` 📖	mathematical	—	`nhdsWithin` `Set.iUnion` `iSup` `Filter` `Filter.instSupSet`	—	`Set.sUnion_range` `nhdsWithin_sUnion` `Set.finite_range` `iSup_range`
`nhdsWithin_insert` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instInsert` `Filter` `Filter.instSup` `Filter.instPure`	—	`Set.singleton_union` `nhdsWithin_union` `nhdsWithin_singleton`
`nhdsWithin_inter` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instInter` `Filter` `Filter.instInf`	—	`inf_left_comm` `inf_assoc` `Filter.inf_principal` `inf_idem`
`nhdsWithin_inter'` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instInter` `Filter` `Filter.instInf` `Filter.principal`	—	`Filter.inf_principal` `inf_assoc`
`nhdsWithin_inter_of_mem` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`nhdsWithin_inter` `inf_eq_right` `nhdsWithin_le_of_mem`
`nhdsWithin_inter_of_mem'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`Set.inter_comm` `nhdsWithin_inter_of_mem`
`nhdsWithin_le_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `Set` `Filter.instMembership`	—	`Filter.set_eventuallyLE_iff_inf_principal_le` `Filter.set_eventuallyLE_iff_mem_inf_principal`
`nhdsWithin_le_nhds` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `nhds`	—	`nhdsWithin_univ` `nhdsWithin_le_of_mem` `Filter.univ_mem`
`nhdsWithin_le_of_mem` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	`nhdsWithin_le_iff`
`nhdsWithin_neBot_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Filter.NeBot` `nhdsWithin`	—	`mem_closure_iff_nhdsWithin_neBot` `subset_closure`
`nhdsWithin_pi_eq` 📖	mathematical	—	`nhdsWithin` `Pi.topologicalSpace` `Set.pi` `Filter` `Filter.instInf` `iInf` `Filter.instInfSet` `Set` `Set.instMembership` `Filter.comap` `nhds`	—	`nhds_pi` `Set.pi_def` `Filter.iInf_principal_finite` `iInf_congr_Prop` `Filter.comap_inf` `Filter.comap_principal` `iInf_split` `inf_right_comm` `iInf_inf_eq`
`nhdsWithin_pi_eq'` 📖	mathematical	—	`nhdsWithin` `Pi.topologicalSpace` `Set.pi` `iInf` `Filter` `Filter.instInfSet` `Filter.comap` `Filter.instInf` `nhds` `Set` `Set.instMembership` `Filter.principal`	—	`nhds_pi` `Set.pi_def` `Filter.iInf_principal_finite` `Filter.comap_inf` `Filter.comap_iInf` `iInf_congr_Prop` `Filter.comap_principal`
`nhdsWithin_pi_eq_bot` 📖	mathematical	—	`nhdsWithin` `Pi.topologicalSpace` `Set.pi` `Bot.bot` `Filter` `Filter.instBot` `Set` `Set.instMembership`	—	`nhds_pi` `nhds_neBot`
`nhdsWithin_pi_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Pi.topologicalSpace` `Set.pi`	—	—
`nhdsWithin_pi_univ_eq` 📖	mathematical	—	`nhdsWithin` `Pi.topologicalSpace` `Set.pi` `Set.univ` `iInf` `Filter` `Filter.instInfSet` `Filter.comap`	—	`Filter.comap_inf` `Filter.comap_principal` `iInf_congr_Prop` `iInf_pos` `iInf_neg` `iInf_top` `inf_of_le_left` `nhdsWithin_pi_eq` `Set.finite_univ`
`nhdsWithin_prod` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`instTopologicalSpaceProd` `SProd.sprod` `Set.instSProd`	—	`nhdsWithin_prod_eq` `Filter.prod_mem_prod`
`nhdsWithin_restrict` 📖	mathematical	`Set` `Set.instMembership` `IsOpen`	`nhdsWithin` `Set.instInter`	—	`nhdsWithin_restrict'` `IsOpen.mem_nhds`
`nhdsWithin_restrict'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `Set.instInter`	—	`nhdsWithin_restrict''` `Filter.mem_inf_of_left`
`nhdsWithin_restrict''` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`le_antisymm` `le_inf` `inf_le_left` `Filter.le_principal_iff` `Filter.inter_mem` `self_mem_nhdsWithin` `inf_le_inf_left` `Filter.principal_mono` `Set.inter_subset_left`
`nhdsWithin_sUnion` 📖	mathematical	—	`nhdsWithin` `Set.sUnion` `iSup` `Filter` `Set` `Filter.instSupSet` `Set.instMembership`	—	`Set.sUnion_eq_biUnion` `nhdsWithin_biUnion`
`nhdsWithin_singleton` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instSingletonSet` `Filter` `Filter.instPure`	—	`nhdsWithin.eq_1` `Filter.principal_singleton` `inf_eq_right` `pure_le_nhds`
`nhdsWithin_subtype` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instMembership` `instTopologicalSpaceSubtype` `Filter.comap` `Set.image`	—	`Filter.ext` `mem_nhdsWithin_subtype`
`nhdsWithin_union` 📖	mathematical	—	`nhdsWithin` `Set` `Set.instUnion` `Filter` `Filter.instSup`	—	`inf_sup_left` `Filter.sup_principal`
`nhdsWithin_univ` 📖	mathematical	—	`nhdsWithin` `Set.univ` `nhds`	—	`nhdsWithin.eq_1` `Filter.principal_univ` `inf_top_eq`
`nhds_bind_nhdsWithin` 📖	mathematical	—	`Filter.bind` `nhds` `nhdsWithin`	—	`Filter.bind_inf_principal` `nhds_bind_nhds`
`nhds_eq_nhdsWithin_sup_nhdsWithin` 📖	mathematical	`Set.univ` `Set` `Set.instUnion`	`nhds` `Filter` `Filter.instSup` `nhdsWithin`	—	`nhdsWithin_univ` `nhdsWithin_union`
`nhds_of_Ici_Iic` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	`nhds` `Set.instUnion` `Set.instInter`	—	`union_mem_nhds_of_mem_nhdsWithin` `Set.Iic_union_Ici` `Filter.inter_mem` `self_mem_nhdsWithin`
`nhds_of_nhdsWithin_of_nhds` 📖	—	`Set` `Filter` `Filter.instMembership` `nhds` `nhdsWithin`	—	—	`mem_nhdsWithin_iff_exists_mem_nhds_inter` `Filter.sets_of_superset` `Filter.inter_sets`
`preimage_coe_mem_nhds_subtype` 📖	mathematical	—	`Set` `Set.Elem` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpaceSubtype` `Set.instMembership` `Set.preimage` `nhdsWithin`	—	`map_nhds_subtype_val` `Filter.mem_map`
`preimage_nhdsWithin_coinduced'` 📖	mathematical	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhds` `TopologicalSpace.coinduced` `Set.Elem` `TopologicalSpace` `instTopologicalSpaceSubtype`	`nhdsWithin` `Set.preimage`	—	`CanLift.prf` `Subtype.canLift` `preimage_nhds_coinduced` `map_nhds_subtype_val` `Filter.mem_map`
`preimage_nhds_within_coinduced` 📖	mathematical	`Set` `Set.instMembership` `IsOpen` `Filter` `Filter.instMembership` `nhds` `TopologicalSpace.coinduced` `Set.Elem` `TopologicalSpace` `instTopologicalSpaceSubtype`	`Set.preimage`	—	`IsOpen.nhdsWithin_eq` `preimage_nhdsWithin_coinduced'`
`principal_inter_le_nhdsSetWithin` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `Set` `Set.instInter` `nhdsSetWithin`	—	`Filter.inf_principal` `inf_le_of_left_le` `principal_le_nhdsSet`
`punctured_nhds_eq_nhdsWithin_sup_nhdsWithin` 📖	mathematical	—	`nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter` `Filter.instSup` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi`	—	`Set.Iio_union_Ioi` `nhdsWithin_union`
`pure_le_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instPure` `nhdsWithin`	—	`le_inf` `pure_le_nhds` `Filter.le_principal_iff`
`pure_sup_nhdsNE` 📖	mathematical	—	`Filter` `Filter.instSup` `Filter.instPure` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`sup_comm` `nhdsNE_sup_pure`
`self_mem_nhdsWithin` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	—	`Filter.mem_inf_of_right` `Filter.mem_principal_self`
`tendsto_const_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership`	`Filter.Tendsto` `nhdsWithin`	—	`Filter.Tendsto.mono_right` `Filter.tendsto_const_pure` `pure_le_nhdsWithin`
`tendsto_nhdsWithin_congr` 📖	—	`Filter.Tendsto` `nhdsWithin`	—	—	`Filter.tendsto_congr'` `eventuallyEq_nhdsWithin_of_eqOn`
`tendsto_nhdsWithin_iff` 📖	mathematical	—	`Filter.Tendsto` `nhdsWithin` `nhds` `Filter.Eventually` `Set` `Set.instMembership`	—	`tendsto_nhds_of_tendsto_nhdsWithin` `eventually_mem_of_tendsto_nhdsWithin` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within`
`tendsto_nhdsWithin_iff_subtype` 📖	mathematical	`Set` `Set.instMembership`	`Filter.Tendsto` `nhdsWithin` `Set.Elem` `Set.restrict` `nhds` `instTopologicalSpaceSubtype`	—	`nhdsWithin_eq_map_subtype_coe` `Filter.tendsto_map'_iff`
`tendsto_nhdsWithin_mono_left` 📖	—	`Set` `Set.instHasSubset` `Filter.Tendsto` `nhdsWithin`	—	—	`Filter.Tendsto.mono_left` `nhdsWithin_mono`
`tendsto_nhdsWithin_mono_right` 📖	—	`Set` `Set.instHasSubset` `Filter.Tendsto` `nhdsWithin`	—	—	`Filter.Tendsto.mono_right` `nhdsWithin_mono`
`tendsto_nhdsWithin_of_tendsto_nhds` 📖	mathematical	`Filter.Tendsto` `nhds`	`nhdsWithin`	—	`Filter.Tendsto.mono_left` `inf_le_left`
`tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` 📖	mathematical	`Filter.Tendsto` `nhds` `Filter.Eventually` `Set` `Set.instMembership`	`nhdsWithin`	—	`Filter.tendsto_inf` `Filter.tendsto_principal`
`tendsto_nhdsWithin_range` 📖	mathematical	—	`Filter.Tendsto` `nhdsWithin` `Set.range` `nhds`	—	`Filter.Tendsto.mono_right` `inf_le_left` `Filter.tendsto_inf` `Filter.tendsto_principal` `Filter.Eventually.of_forall` `Set.mem_range_self`
`tendsto_nhds_of_tendsto_nhdsWithin` 📖	mathematical	`Filter.Tendsto` `nhdsWithin`	`nhds`	—	`Filter.Tendsto.mono_right` `nhdsWithin_le_nhds`
`union_mem_nhds_of_mem_nhdsWithin` 📖	mathematical	`Set.univ` `Set` `Set.instUnion` `Filter` `Filter.instMembership` `nhdsWithin`	`nhds`	—	`nhdsWithin_univ` `nhdsWithin_union` `Filter.mem_of_superset`

---

← Back to Index