ClusterPt

📁 Source: Mathlib/Topology/ClusterPt.lean

Statistics

Metric	Count
Definitions `ClusterPt`	1
Theorems `clusterPt`, `mono`, `frequently`, `frequently'`, `mapClusterPt_id`, `mem_closure`, `mem_closure_of_mem`, `mono`, `neBot`, `of_inf_left`, `of_inf_right`, `of_le_nhds`, `of_le_nhds'`, `of_nhds_le`, `top`, `mapClusterPt`, `mapClusterPt_iff`, `clusterPt_iff`, `clusterPt_iff_forall_mem_closure`, `clusterPt_iff_frequently`, `clusterPt_iff_frequently'`, `mapClusterPt_iff_frequently`, `mapClusterPt`, `mem_of_mapClusterPt`, `clusterPt`, `congrFun`, `continuousAt_comp`, `frequently`, `mono`, `of_comp`, `tendsto_comp`, `tendsto_comp'`, `accPt_iff_clusterPt`, `accPt_iff_frequently`, `accPt_iff_frequently_nhdsNE`, `accPt_iff_nhds`, `accPt_principal_iff_clusterPt`, `accPt_principal_iff_nhdsWithin`, `accPt_sup`, `closure_compl_singleton`, `closure_eq_cluster_pts`, `clusterPt_iff_forall_mem_closure`, `clusterPt_iff_frequently`, `clusterPt_iff_frequently'`, `clusterPt_iff_lift'_closure`, `clusterPt_iff_lift'_closure'`, `clusterPt_iff_nonempty`, `clusterPt_iff_not_disjoint`, `clusterPt_lift'_closure_iff`, `clusterPt_principal`, `clusterPt_principal_iff`, `clusterPt_principal_iff_frequently`, `clusterPt_sup`, `dense_compl_singleton`, `interior_singleton`, `isClosed_iff_clusterPt`, `isClosed_iff_forall_filter`, `isClosed_iff_nhds`, `isClosed_setOf_clusterPt`, `mapClusterPt_comp`, `mapClusterPt_def`, `mapClusterPt_id_iff`, `mapClusterPt_iff_frequently`, `mem_closure_iff_clusterPt`, `mem_closure_iff_comap_neBot`, `mem_closure_iff_nhds`, `mem_closure_iff_nhds'`, `mem_closure_iff_nhdsWithin_neBot`, `mem_closure_iff_nhds_basis`, `mem_closure_iff_nhds_basis'`, `mem_closure_iff_nhds_ne_bot`, `mem_closure_of_mem_closure_union`, `mem_interior_iff_not_clusterPt_compl`, `notMem_closure_iff_nhdsWithin_eq_bot`, `not_isOpen_singleton`	75
Total	76

AccPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt` 📖	mathematical	—	`ClusterPt`	—	`ClusterPt.mono` `accPt_iff_clusterPt` `inf_le_right`
`mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`AccPt`	—	`Filter.NeBot.mono` `inf_le_inf_left`

ClusterPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`frequently` 📖	mathematical	`Filter.Eventually` `nhds`	`Filter.Frequently`	—	`clusterPt_iff_frequently`
`frequently'` 📖	mathematical	`Filter.Eventually`	`Filter.Frequently` `nhds`	—	`clusterPt_iff_frequently'`
`mapClusterPt_id` 📖	mathematical	—	`MapClusterPt`	—	`mapClusterPt_id_iff`
`mem_closure` 📖	mathematical	—	`Set` `Set.instMembership` `closure`	—	`mem_closure_iff_clusterPt`
`mem_closure_of_mem` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`Set.instMembership` `closure`	—	`clusterPt_iff_forall_mem_closure`
`mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`ClusterPt`	—	`Filter.NeBot.mono` `inf_le_inf_left`
`neBot` 📖	mathematical	—	`Filter.NeBot` `Filter` `Filter.instInf` `nhds`	—	—
`of_inf_left` 📖	mathematical	—	`ClusterPt`	—	`mono` `inf_le_left`
`of_inf_right` 📖	mathematical	—	`ClusterPt`	—	`mono` `inf_le_right`
`of_le_nhds` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`ClusterPt`	—	`eq_1` `inf_eq_right`
`of_le_nhds'` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`ClusterPt`	—	`of_le_nhds`
`of_nhds_le` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`ClusterPt`	—	`inf_eq_left`
`top` 📖	mathematical	—	`ClusterPt` `Top.top` `Filter` `Filter.instTop`	—	`inf_of_le_left`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapClusterPt` 📖	mathematical	`ContinuousAt`	`MapClusterPt`	—	`MapClusterPt.continuousAt_comp` `ClusterPt.mapClusterPt_id`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapClusterPt_iff` 📖	mathematical	`Filter.EventuallyEq`	`MapClusterPt`	—	`Filter.map_congr`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt_iff` 📖	mathematical	`Filter.HasBasis` `nhds`	`ClusterPt` `Set.Nonempty` `Set` `Set.instInter`	—	`inf_basis_neBot_iff`
`clusterPt_iff_forall_mem_closure` 📖	mathematical	`Filter.HasBasis`	`ClusterPt` `Set` `Set.instMembership` `closure`	—	`clusterPt_iff` `nhds_basis_opens`
`clusterPt_iff_frequently` 📖	mathematical	`Filter.HasBasis` `nhds`	`ClusterPt` `Filter.Frequently` `Set` `Set.instMembership`	—	`clusterPt_iff` `Filter.basis_sets` `Set.inter_comm`
`clusterPt_iff_frequently'` 📖	mathematical	`Filter.HasBasis`	`ClusterPt` `Filter.Frequently` `Set` `Set.instMembership` `nhds`	—	`clusterPt_iff` `Filter.basis_sets`
`mapClusterPt_iff_frequently` 📖	mathematical	`Filter.HasBasis` `nhds`	`MapClusterPt` `Filter.Frequently` `Set` `Set.instMembership`	—	`clusterPt_iff_frequently`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapClusterPt` 📖	mathematical	`Filter.Tendsto` `nhds`	`MapClusterPt`	—	`ClusterPt.of_le_nhds` `Filter.map_neBot`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_of_mapClusterPt` 📖	—	`Filter.Eventually` `Set` `Set.instMembership`	—	—	`Filter.Frequently.mem_of_closed` `ClusterPt.frequently'`

MapClusterPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt` 📖	mathematical	—	`ClusterPt` `Filter.map`	—	`mapClusterPt_def`
`congrFun` 📖	mathematical	`Filter.EventuallyEq`	`MapClusterPt`	—	`Filter.EventuallyEq.mapClusterPt_iff`
`continuousAt_comp` 📖	mathematical	`ContinuousAt`	`MapClusterPt`	—	`tendsto_comp`
`frequently` 📖	mathematical	`Filter.Eventually` `nhds`	`Filter.Frequently`	—	`ClusterPt.frequently` `clusterPt`
`mono` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`MapClusterPt`	—	`ClusterPt.mono` `clusterPt` `Filter.map_mono`
`of_comp` 📖	mathematical	`Filter.Tendsto`	`MapClusterPt`	—	`ClusterPt.mono` `clusterPt` `Filter.map_mono`
`tendsto_comp` 📖	mathematical	`Filter.Tendsto` `nhds`	`MapClusterPt`	—	`tendsto_comp'` `Filter.Tendsto.mono_left` `inf_le_left`
`tendsto_comp'` 📖	mathematical	`Filter.Tendsto` `Filter` `Filter.instInf` `nhds` `Filter.map`	`MapClusterPt`	—	`Filter.Tendsto.neBot` `Filter.tendsto_inf` `Filter.Tendsto.mono_left` `Filter.tendsto_map` `inf_le_right`

(root)

Definitions

Name	Category	Theorems
`ClusterPt` 📖	MathDef	56 math math: `Filter.HasBasis.clusterPt_iff_frequently'`, `le_nhds_iff_adhp_of_cauchy`, `Ultrafilter.clusterPt_iff`, `clusterPt_sup`, `clusterPt_principal_iff`, `ClusterPt.mono`, `Filter.TotallyBounded.exists_clusterPt`, `closure_eq_cluster_pts`, `mapClusterPt_id_iff`, `isOpenMap_iff_clusterPt_comap`, `mapClusterPt_def`, `isProperMap_iff_clusterPt`, `ClusterPt.of_le_nhds`, `MapClusterPt.clusterPt`, `Specializes.clusterPt`, `clusterPt_iff_frequently'`, `ClusterPt.top`, `Filter.HasBasis.clusterPt_iff_frequently`, `clusterPt_iff_lift'_closure'`, `Filter.TotallyBounded.isCompact_setOf_clusterPt`, `ClusterPt.of_le_nhds'`, `mem_interior_iff_not_clusterPt_compl`, `IsCompact.exists_clusterPt`, `mem_closure_iff_clusterPt`, `clusterPt_iff_frequently`, `clusterPt_iff_not_disjoint`, `tangentConeAt_def`, `isClosed_setOf_clusterPt`, `clusterPt_lift'_closure_iff`, `IsProperMap.clusterPt_of_mapClusterPt`, `exists_clusterPt_of_compactSpace`, `AccPt.clusterPt`, `ClusterPt.map`, `isComplete_iff_clusterPt`, `clusterPt_iff_nonempty`, `isClosedMap_iff_clusterPt`, `clusterPt_iff_forall_mem_closure`, `IsOpenMap.clusterPt_comap`, `specializes_iff_clusterPt`, `cluster_point_of_Lindelof`, `ClusterPt.of_nhds_le`, `inseparable_iff_clusterPt_uniformity`, `Filter.TotallyBounded.totallyBounded_setOf_clusterPt`, `clusterPt_iff_lift'_closure`, `clusterPt_principal`, `clusterPt_iff_ultrafilter`, `accPt_principal_iff_clusterPt`, `Filter.HasBasis.clusterPt_iff`, `IsCompact.exists_clusterPt_of_frequently`, `ClusterPt.of_inf_left`, `clusterPt_principal_iff_frequently`, `Topology.IsInducing.mapClusterPt_iff`, `accPt_iff_clusterPt`, `ClusterPt.of_inf_right`, `Filter.HasBasis.clusterPt_iff_forall_mem_closure`, `specializes_TFAE`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accPt_iff_clusterPt` 📖	mathematical	—	`AccPt` `ClusterPt` `Filter` `Filter.instInf` `Filter.principal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`AccPt.eq_1` `nhdsWithin.eq_1` `ClusterPt.eq_1` `inf_assoc`
`accPt_iff_frequently` 📖	mathematical	—	`AccPt` `Filter.principal` `Filter.Frequently` `Set` `Set.instMembership` `nhds`	—	—
`accPt_iff_frequently_nhdsNE` 📖	mathematical	—	`AccPt` `Filter.principal` `Filter.Frequently` `Set` `Set.instMembership` `nhdsWithin` `Compl.compl` `Set.instCompl` `Set.instSingletonSet`	—	`Filter.frequently_inf_principal` `accPt_iff_frequently`
`accPt_iff_nhds` 📖	mathematical	—	`AccPt` `Filter.principal` `Set` `Set.instMembership` `Set.instInter`	—	—
`accPt_principal_iff_clusterPt` 📖	mathematical	—	`AccPt` `Filter.principal` `ClusterPt` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`accPt_iff_clusterPt` `Filter.inf_principal` `Set.inter_comm` `Set.diff_eq`
`accPt_principal_iff_nhdsWithin` 📖	mathematical	—	`AccPt` `Filter.principal` `Filter.NeBot` `nhdsWithin` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`accPt_principal_iff_clusterPt` `ClusterPt.eq_1` `nhdsWithin.eq_1`
`accPt_sup` 📖	mathematical	—	`AccPt` `Filter` `Filter.instSup`	—	`inf_sup_left`
`closure_compl_singleton` 📖	mathematical	—	`closure` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Set.univ`	—	`Dense.closure_eq` `dense_compl_singleton`
`closure_eq_cluster_pts` 📖	mathematical	—	`closure` `setOf` `ClusterPt` `Filter.principal`	—	`Set.ext` `mem_closure_iff_clusterPt`
`clusterPt_iff_forall_mem_closure` 📖	mathematical	—	`ClusterPt` `Set` `Set.instMembership` `closure`	—	`Filter.HasBasis.clusterPt_iff_forall_mem_closure` `Filter.basis_sets`
`clusterPt_iff_frequently` 📖	mathematical	—	`ClusterPt` `Filter.Frequently` `Set` `Set.instMembership`	—	`Filter.HasBasis.clusterPt_iff_frequently` `Filter.basis_sets`
`clusterPt_iff_frequently'` 📖	mathematical	—	`ClusterPt` `Filter.Frequently` `Set` `Set.instMembership` `nhds`	—	`Filter.HasBasis.clusterPt_iff_frequently'` `Filter.basis_sets`
`clusterPt_iff_lift'_closure` 📖	mathematical	—	`ClusterPt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instPure` `Filter.lift'` `closure`	—	`Filter.HasBasis.le_basis_iff` `Filter.hasBasis_pure` `Filter.HasBasis.lift'_closure` `Filter.basis_sets`
`clusterPt_iff_lift'_closure'` 📖	mathematical	—	`ClusterPt` `Filter.NeBot` `Filter` `Filter.instInf` `Filter.lift'` `closure` `Filter.instPure`	—	`clusterPt_iff_lift'_closure` `inf_comm` `inf_of_le_left`
`clusterPt_iff_nonempty` 📖	mathematical	—	`ClusterPt` `Set.Nonempty` `Set` `Set.instInter`	—	`Filter.inf_neBot_iff`
`clusterPt_iff_not_disjoint` 📖	mathematical	—	`ClusterPt` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds`	—	`disjoint_iff` `ClusterPt.eq_1` `Filter.neBot_iff`
`clusterPt_lift'_closure_iff` 📖	mathematical	—	`ClusterPt` `Filter.lift'` `closure`	—	`Filter.lift'_lift'_assoc` `monotone_closure` `IsClosed.closure_eq`
`clusterPt_principal` 📖	mathematical	—	`ClusterPt` `Filter.principal` `Set` `Set.instMembership` `AccPt`	—	`accPt_principal_iff_clusterPt` `Set.diff_singleton_eq_self` `clusterPt_principal_iff` `mem_of_mem_nhds` `AccPt.clusterPt`
`clusterPt_principal_iff` 📖	mathematical	—	`ClusterPt` `Filter.principal` `Set.Nonempty` `Set` `Set.instInter`	—	`Filter.inf_principal_neBot_iff`
`clusterPt_principal_iff_frequently` 📖	mathematical	—	`ClusterPt` `Filter.principal` `Filter.Frequently` `Set` `Set.instMembership` `nhds`	—	—
`clusterPt_sup` 📖	mathematical	—	`ClusterPt` `Filter` `Filter.instSup`	—	`inf_sup_left`
`dense_compl_singleton` 📖	mathematical	—	`Dense` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`eq_or_ne` `mem_closure_iff_nhdsWithin_neBot` `subset_closure`
`interior_singleton` 📖	mathematical	—	`interior` `Set` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`interior_eq_empty_iff_dense_compl` `dense_compl_singleton`
`isClosed_iff_clusterPt` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	`closure_subset_iff_isClosed`
`isClosed_iff_forall_filter` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	`Filter.NeBot.mono` `le_inf` `inf_le_right` `inf_le_left`
`isClosed_iff_nhds` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	—
`isClosed_setOf_clusterPt` 📖	mathematical	—	`IsClosed` `setOf` `ClusterPt`	—	`Set.setOf_forall` `isClosed_biInter` `isClosed_closure`
`mapClusterPt_comp` 📖	mathematical	—	`MapClusterPt` `Filter.map`	—	—
`mapClusterPt_def` 📖	mathematical	—	`MapClusterPt` `ClusterPt` `Filter.map`	—	—
`mapClusterPt_id_iff` 📖	mathematical	—	`MapClusterPt` `ClusterPt`	—	`MapClusterPt.eq_1` `Filter.map_id`
`mapClusterPt_iff_frequently` 📖	mathematical	—	`MapClusterPt` `Filter.Frequently` `Set` `Set.instMembership`	—	`Filter.HasBasis.mapClusterPt_iff_frequently` `Filter.basis_sets`
`mem_closure_iff_clusterPt` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `ClusterPt` `Filter.principal`	—	`mem_closure_iff_frequently` `clusterPt_principal_iff_frequently`
`mem_closure_iff_comap_neBot` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Filter.NeBot` `Filter.comap` `nhds`	—	—
`mem_closure_iff_nhds` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Set.Nonempty` `Set.instInter`	—	`mem_closure_iff_clusterPt` `clusterPt_principal_iff`
`mem_closure_iff_nhds'` 📖	mathematical	—	`Set` `Set.instMembership` `closure`	—	—
`mem_closure_iff_nhdsWithin_neBot` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Filter.NeBot` `nhdsWithin`	—	`mem_closure_iff_clusterPt`
`mem_closure_iff_nhds_basis` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `closure`	—	`mem_closure_iff_nhds_basis'`
`mem_closure_iff_nhds_basis'` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `closure` `Set.Nonempty` `Set.instInter`	—	`mem_closure_iff_clusterPt` `Filter.HasBasis.clusterPt_iff` `Filter.hasBasis_principal`
`mem_closure_iff_nhds_ne_bot` 📖	mathematical	—	`Set` `Set.instMembership` `closure`	—	`mem_closure_iff_clusterPt` `Filter.neBot_iff`
`mem_closure_of_mem_closure_union` 📖	—	`Set` `Set.instMembership` `closure` `Set.instUnion` `Filter` `Filter.instMembership` `nhds` `Compl.compl` `Set.instCompl`	—	—	`mem_closure_iff_nhds_ne_bot` `bot_sup_eq` `Filter.inf_principal_eq_bot` `inf_sup_left` `Filter.sup_principal`
`mem_interior_iff_not_clusterPt_compl` 📖	mathematical	—	`Set` `Set.instMembership` `interior` `ClusterPt` `Filter.principal` `Compl.compl` `Set.instCompl`	—	`mem_closure_iff_clusterPt` `closure_compl` `Set.mem_compl_iff`
`notMem_closure_iff_nhdsWithin_eq_bot` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `nhdsWithin` `Bot.bot` `Filter` `Filter.instBot`	—	`mem_closure_iff_nhdsWithin_neBot` `Filter.not_neBot`
`not_isOpen_singleton` 📖	mathematical	—	`IsOpen` `Set` `Set.instSingletonSet`	—	`dense_compl_singleton_iff_not_open` `dense_compl_singleton`

---

← Back to Index