Neighborhoods

📁 Source: Mathlib/Topology/Neighborhoods.lean

Statistics

Metric	Count
Definitions	0
Theorems `inter_nhds_nonempty`, `inter_of_isOpen_left`, `inter_of_isOpen_right`, `open_subset_closure_inter`, `eventually_nhds`, `self_of_nhds`, `eq_of_nhds`, `eventuallyEq_nhds`, `tendsto`, `eventuallyLE_nhds`, `mem_closure`, `mem_of_closed`, `nhds_interior`, `compl_mem_nhds`, `interior_union_left`, `interior_union_right`, `mem_of_frequently_of_tendsto`, `mem_of_tendsto`, `closure_inter`, `eventually_mem`, `inter_closure`, `mem_nhds`, `mem_nhds_iff`, `tendsto_atTop_nhds`, `ext_iff_nhds`, `ext_nhds`, `all_mem_nhds`, `all_mem_nhds_filter`, `closure_diff`, `eventually_eventuallyEq_nhds`, `eventually_eventuallyLE_nhds`, `eventually_eventually_nhds`, `eventually_mem_nhds_iff`, `eventually_nhds_iff`, `exists_open_set_nhds`, `exists_open_set_nhds'`, `frequently_frequently_nhds`, `frequently_nhds_iff`, `interior_eq_nhds`, `interior_eq_nhds'`, `interior_mem_nhds`, `interior_setOf_eq`, `isClosed_iff_frequently`, `isOpen_iff_eventually`, `isOpen_iff_mem_nhds`, `isOpen_iff_nhds`, `isOpen_setOf_eventually_nhds`, `isOpen_singleton_iff_nhds_eq_pure`, `isOpen_singleton_iff_punctured_nhds`, `le_nhds_iff`, `lift'_nhds_interior`, `map_nhds`, `mem_closure_iff_frequently`, `mem_closure_of_frequently_of_tendsto`, `mem_closure_of_tendsto`, `mem_interior_iff_mem_nhds`, `mem_nhds_iff`, `mem_of_mem_nhds`, `nhdsWithin_mono`, `nhdsWithin_neBot`, `nhds_basis_closeds`, `nhds_basis_opens`, `nhds_basis_opens'`, `nhds_bind_nhds`, `nhds_def'`, `nhds_le_of_le`, `nhds_neBot`, `pure_le_nhds`, `subset_interior_iff_nhds`, `tendsto_atBot_of_eventually_const`, `tendsto_atTop_nhds`, `tendsto_atTop_of_eventually_const`, `tendsto_const_nhds`, `tendsto_inf_principal_nhds_iff_of_forall_eq`, `tendsto_nhds`, `tendsto_nhds_of_eventually_eq`, `tendsto_pure_nhds`	77
Total	77

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_nhds_nonempty` 📖	mathematical	`Dense` `Set` `Filter` `Filter.instMembership` `nhds`	`Set.Nonempty` `Set.instInter`	—	`mem_nhds_iff` `Set.Nonempty.mono` `inter_open_nonempty`
`inter_of_isOpen_left` 📖	mathematical	`Dense` `IsOpen`	`Set` `Set.instInter`	—	`closure_minimal` `IsOpen.inter_closure` `isClosed_closure` `closure_eq` `Set.inter_univ`
`inter_of_isOpen_right` 📖	mathematical	`Dense` `IsOpen`	`Set` `Set.instInter`	—	`inter_of_isOpen_left` `Set.inter_comm`
`open_subset_closure_inter` 📖	mathematical	`Dense` `IsOpen`	`Set` `Set.instHasSubset` `closure` `Set.instInter`	—	`closure_eq` `Set.inter_univ` `IsOpen.inter_closure`

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nhds` 📖	—	`Filter.Eventually` `nhds`	—	—	`eventually_nhds_iff`
`self_of_nhds` 📖	—	`Filter.Eventually` `nhds`	—	—	`mem_of_mem_nhds`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_nhds` 📖	—	`Filter.EventuallyEq` `nhds`	—	—	`Filter.Eventually.self_of_nhds`
`eventuallyEq_nhds` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`Filter.Eventually`	—	`Filter.Eventually.eventually_nhds`
`tendsto` 📖	mathematical	`Filter.EventuallyEq`	`Filter.Tendsto` `nhds`	—	`tendsto_nhds_of_eventually_eq`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyLE_nhds` 📖	mathematical	`Filter.EventuallyLE` `nhds`	`Filter.Eventually`	—	`Filter.Eventually.eventually_nhds`

Filter.Frequently

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_closure` 📖	mathematical	`Filter.Frequently` `Set` `Set.instMembership` `nhds`	`closure`	—	`mem_closure_iff_frequently`
`mem_of_closed` 📖	—	`Filter.Frequently` `Set` `Set.instMembership` `nhds`	—	—	`IsClosed.closure_subset` `mem_closure`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds_interior` 📖	mathematical	`Filter.HasBasis` `nhds`	`interior`	—	`lift'_interior` `lift'_nhds_interior`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_mem_nhds` 📖	mathematical	`Set` `Set.instMembership`	`Filter` `Filter.instMembership` `nhds` `Compl.compl` `Set.instCompl`	—	`IsOpen.mem_nhds` `isOpen_compl` `Set.mem_compl`
`interior_union_left` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `Set.instUnion`	—	`mem_interior` `IsOpen.inter` `isOpen_compl`
`interior_union_right` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `Set.instUnion`	—	`Set.union_comm` `interior_union_left`
`mem_of_frequently_of_tendsto` 📖	—	`Filter.Frequently` `Set` `Set.instMembership` `Filter.Tendsto` `nhds`	—	—	`Filter.Frequently.mem_of_closed` `Filter.Tendsto.frequently`
`mem_of_tendsto` 📖	—	`Filter.Tendsto` `nhds` `Filter.Eventually` `Set` `Set.instMembership`	—	—	`mem_of_frequently_of_tendsto` `Filter.Eventually.frequently`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_inter` 📖	mathematical	`IsOpen`	`Set` `Set.instHasSubset` `Set.instInter` `closure`	—	`Set.inter_comm` `inter_closure`
`eventually_mem` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`Filter.Eventually` `nhds`	—	`mem_nhds`
`inter_closure` 📖	mathematical	`IsOpen`	`Set` `Set.instHasSubset` `Set.instInter` `closure`	—	`Set.compl_subset_compl` `Set.compl_inter` `IsClosed.interior_union_left` `isClosed_compl`
`mem_nhds` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`Filter` `Filter.instMembership` `nhds`	—	`mem_nhds_iff` `Set.Subset.refl`
`mem_nhds_iff` 📖	mathematical	`IsOpen`	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership`	—	`mem_of_mem_nhds` `mem_nhds_iff` `Set.Subset.rfl`

OrderTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_atTop_nhds` 📖	mathematical	—	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `nhds` `Top.top` `toTop` `Preorder.toLE`	—	`Filter.Tendsto.mono_right` `Filter.tendsto_atTop_pure` `pure_le_nhds`

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_iff_nhds` 📖	mathematical	—	`nhds`	—	`ext` `isOpen_iff_nhds`
`ext_nhds` 📖	—	`nhds`	—	—	`ext_iff_nhds`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all_mem_nhds` 📖	—	—	—	—	`Filter.HasBasis.forall_iff` `nhds_basis_opens`
`all_mem_nhds_filter` 📖	mathematical	`Set` `Set.instHasSubset`	`Filter` `Filter.instMembership`	—	`all_mem_nhds` `Filter.mem_of_superset`
`closure_diff` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.instSDiff` `closure`	—	`Set.inter_comm` `IsOpen.inter_closure` `isOpen_compl_iff` `isClosed_closure` `closure_mono` `Set.diff_subset_diff` `Set.Subset.refl` `subset_closure`
`eventually_eventuallyEq_nhds` 📖	mathematical	—	`Filter.Eventually` `Filter.EventuallyEq` `nhds`	—	`eventually_eventually_nhds`
`eventually_eventuallyLE_nhds` 📖	mathematical	—	`Filter.Eventually` `Filter.EventuallyLE` `nhds`	—	`eventually_eventually_nhds`
`eventually_eventually_nhds` 📖	mathematical	—	`Filter.Eventually` `nhds`	—	`Filter.Eventually.self_of_nhds` `Filter.Eventually.eventually_nhds`
`eventually_mem_nhds_iff` 📖	mathematical	—	`Filter.Eventually` `Set` `Filter` `Filter.instMembership` `nhds`	—	`eventually_eventually_nhds`
`eventually_nhds_iff` 📖	mathematical	—	`Filter.Eventually` `nhds` `IsOpen` `Set` `Set.instMembership`	—	`mem_nhds_iff`
`exists_open_set_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`Set.instHasSubset` `IsOpen`	—	`mem_interior_iff_mem_nhds` `isOpen_interior` `interior_subset`
`exists_open_set_nhds'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `iSup` `Filter.instSupSet` `Set.instMembership` `nhds`	`Set.instHasSubset` `IsOpen`	—	`exists_open_set_nhds`
`frequently_frequently_nhds` 📖	mathematical	—	`Filter.Frequently` `nhds`	—	`not_iff_not`
`frequently_nhds_iff` 📖	mathematical	—	`Filter.Frequently` `nhds` `Set` `Set.instMembership`	—	`Filter.HasBasis.frequently_iff` `nhds_basis_opens`
`interior_eq_nhds` 📖	mathematical	—	`interior` `setOf` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.principal`	—	`interior_eq_nhds'`
`interior_eq_nhds'` 📖	mathematical	—	`interior` `setOf` `Set` `Filter` `Filter.instMembership` `nhds`	—	`Set.ext`
`interior_mem_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `interior`	—	`Filter.mem_of_superset` `interior_subset` `IsOpen.mem_nhds` `isOpen_interior` `mem_interior_iff_mem_nhds`
`interior_setOf_eq` 📖	mathematical	—	`interior` `setOf` `Filter.Eventually` `nhds`	—	`interior_eq_nhds'`
`isClosed_iff_frequently` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	`closure_subset_iff_isClosed` `mem_closure_iff_frequently`
`isOpen_iff_eventually` 📖	mathematical	—	`IsOpen` `Filter.Eventually` `Set` `Set.instMembership` `nhds`	—	`isOpen_iff_mem_nhds`
`isOpen_iff_mem_nhds` 📖	mathematical	—	`IsOpen` `Set` `Filter` `Filter.instMembership` `nhds`	—	`isOpen_iff_nhds` `Filter.le_principal_iff`
`isOpen_iff_nhds` 📖	mathematical	—	`IsOpen` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.principal`	—	`subset_interior_iff_isOpen` `interior_eq_nhds`
`isOpen_setOf_eventually_nhds` 📖	mathematical	—	`IsOpen` `setOf` `Filter.Eventually` `nhds`	—	—
`isOpen_singleton_iff_nhds_eq_pure` 📖	mathematical	—	`IsOpen` `Set` `Set.instSingletonSet` `nhds` `Filter` `Filter.instPure`	—	`LE.le.ge_iff_eq'` `pure_le_nhds`
`isOpen_singleton_iff_punctured_nhds` 📖	mathematical	—	`IsOpen` `Set` `Set.instSingletonSet` `nhdsWithin` `Compl.compl` `Set.instCompl` `Bot.bot` `Filter` `Filter.instBot`	—	`isOpen_singleton_iff_nhds_eq_pure` `nhdsWithin.eq_1` `Filter.mem_iff_inf_principal_compl` `le_antisymm_iff` `pure_le_nhds`
`le_nhds_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Set` `Filter.instMembership`	—	`nhds_def`
`lift'_nhds_interior` 📖	mathematical	—	`Filter.lift'` `nhds` `interior`	—	`Filter.HasBasis.lift'_interior_eq_self` `nhds_basis_opens`
`map_nhds` 📖	mathematical	—	`Filter.map` `nhds` `iInf` `Filter` `Set` `Filter.instInfSet` `Set.instMembership` `setOf` `IsOpen` `Filter.principal` `Set.image`	—	`Filter.HasBasis.eq_biInf` `Filter.HasBasis.map` `nhds_basis_opens`
`mem_closure_iff_frequently` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Filter.Frequently` `nhds`	—	`Filter.Frequently.eq_1` `Filter.Eventually.eq_1` `mem_interior_iff_mem_nhds` `closure_eq_compl_interior_compl` `Set.mem_compl_iff` `Set.compl_def`
`mem_closure_of_frequently_of_tendsto` 📖	mathematical	`Filter.Frequently` `Set` `Set.instMembership` `Filter.Tendsto` `nhds`	`closure`	—	`Filter.Frequently.mem_closure` `Filter.Tendsto.frequently`
`mem_closure_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhds` `Filter.Eventually` `Set` `Set.instMembership`	`closure`	—	`mem_closure_of_frequently_of_tendsto` `Filter.Eventually.frequently`
`mem_interior_iff_mem_nhds` 📖	mathematical	—	`Set` `Set.instMembership` `interior` `Filter` `Filter.instMembership` `nhds`	—	`mem_interior` `mem_nhds_iff`
`mem_nhds_iff` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Set.instHasSubset` `IsOpen` `Set.instMembership`	—	`Filter.HasBasis.mem_iff` `nhds_basis_opens`
`mem_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`Set.instMembership`	—	`mem_nhds_iff`
`nhdsWithin_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin`	—	`inf_le_inf_left` `Filter.principal_mono`
`nhdsWithin_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Set.Nonempty` `Set` `Set.instInter`	—	`nhdsWithin.eq_1` `Filter.inf_neBot_iff` `Filter.mem_principal_self` `Set.Nonempty.mono` `Set.inter_subset_inter_right`
`nhds_basis_closeds` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Set.instMembership` `IsClosed` `Compl.compl` `Set.instCompl`	—	`Filter.HasBasis.mem_iff` `nhds_basis_opens` `Function.Surjective.exists` `compl_surjective`
`nhds_basis_opens` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Set.instMembership` `IsOpen`	—	`nhds_def` `Filter.hasBasis_biInf_principal` `IsOpen.inter` `Set.inter_subset_left` `Set.inter_subset_right` `Set.mem_univ` `isOpen_univ`
`nhds_basis_opens'` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `IsOpen`	—	`IsOpen.mem_nhds_iff` `nhds_basis_opens`
`nhds_bind_nhds` 📖	mathematical	—	`Filter.bind` `nhds`	—	`Filter.ext` `eventually_eventually_nhds`
`nhds_def'` 📖	mathematical	—	`nhds` `iInf` `Filter` `Set` `Filter.instInfSet` `IsOpen` `Set.instMembership` `Filter.principal`	—	`nhds_def` `iInf_congr_Prop` `iInf_and`
`nhds_le_of_le` 📖	mathematical	`Set` `Set.instMembership` `IsOpen` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal`	`nhds`	—	`nhds_def` `iInf₂_le_of_le`
`nhds_neBot` 📖	mathematical	—	`Filter.NeBot` `nhds`	—	`Filter.neBot_of_le` `Filter.pure_neBot` `pure_le_nhds`
`pure_le_nhds` 📖	mathematical	—	`Pi.hasLe` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instPure` `nhds`	—	`Filter.mem_pure` `mem_of_mem_nhds`
`subset_interior_iff_nhds` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `Filter` `Filter.instMembership` `nhds`	—	—
`tendsto_atBot_of_eventually_const` 📖	mathematical	—	`Filter.Tendsto` `Filter.atBot` `nhds`	—	`tendsto_atTop_of_eventually_const`
`tendsto_atTop_nhds` 📖	mathematical	—	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `Set` `Set.instMembership`	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `SemilatticeSup.instIsDirectedOrder` `nhds_basis_opens`
`tendsto_atTop_of_eventually_const` 📖	mathematical	—	`Filter.Tendsto` `Filter.atTop` `nhds`	—	`Filter.Tendsto.congr'` `Filter.EventuallyEq.symm` `Filter.Eventually.mono` `Filter.eventually_ge_atTop` `tendsto_const_nhds`
`tendsto_const_nhds` 📖	mathematical	—	`Filter.Tendsto` `nhds`	—	`tendsto_nhds` `Filter.univ_mem'`
`tendsto_inf_principal_nhds_iff_of_forall_eq` 📖	mathematical	—	`Filter.Tendsto` `Filter` `Filter.instInf` `Filter.principal` `nhds`	—	`Filter.tendsto_iff_comap` `mem_of_mem_nhds` `sup_le` `sup_le_iff` `inf_top_eq` `Filter.principal_univ` `Set.union_compl_self` `Filter.sup_principal` `sup_inf_right` `le_trans` `inf_le_left`
`tendsto_nhds` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Set` `Filter` `Filter.instMembership` `Set.preimage`	—	`all_mem_nhds_filter` `Set.preimage_mono`
`tendsto_nhds_of_eventually_eq` 📖	mathematical	`Filter.Eventually`	`Filter.Tendsto` `nhds`	—	`Filter.Tendsto.congr'` `Filter.EventuallyEq.symm` `tendsto_const_nhds`
`tendsto_pure_nhds` 📖	mathematical	—	`Filter.Tendsto` `Filter` `Filter.instPure` `nhds`	—	`Filter.Tendsto.mono_right` `Filter.tendsto_pure_pure` `pure_le_nhds`

---

← Back to Index