Documentation Verification Report

Ultrafilter

📁 Source: Mathlib/Topology/Ultrafilter.lean

Statistics

Metric	Count
Definitions `Ultrafilter`	1
Theorems `clusterPt_iff`, `clusterPt_iff_ultrafilter`, `continuousAt_iff_ultrafilter`, `continuous_iff_ultrafilter`, `isClosed_iff_ultrafilter`, `isOpen_iff_ultrafilter`, `mapClusterPt_iff_ultrafilter`, `mem_closure_iff_ultrafilter`	8
Total	9

Ultrafilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt_iff` 📖	mathematical	—	`ClusterPt` `toFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	—	`le_of_inf_neBot'` `ClusterPt.of_le_nhds` `neBot`

(root)

Definitions

Name	Category	Theorems
`Ultrafilter` 📖	CompData	65 math math: `Ultrafilter.finite_biUnion_mem_iff`, `Hindman.exists_idempotent_ultrafilter_le_FP`, `Ultrafilter.mem_pure`, `Filter.mem_iff_ultrafilter`, `Filter.notMem_hyperfilter_of_finite`, `ultrafilter_compact`, `Ultrafilter.coe_pure`, `Ultrafilter.diff_mem_iff`, `Compactum.instT2SpaceA`, `denseRange_pure`, `Hindman.exists_idempotent_ultrafilter_le_FS`, `isOpen_iff_ultrafilter`, `Set.Finite.compl_mem_hyperfilter`, `induced_topology_pure`, `Ultrafilter.union_mem_iff`, `Compactum.cl_eq_closure`, `Compactum.instCompactSpaceA`, `ultrafilter_extend_extends`, `Filter.iSup_ultrafilter_le_eq`, `Ultrafilter.eventually_mul`, `isDenseEmbedding_pure`, `Ultrafilter.map_pure`, `Ultrafilter.mem_or_compl_mem`, `Compactum.le_nhds_of_str_eq`, `Ultrafilter.continuous_add_left`, `Ultrafilter.mem_map`, `Compactum.lim_eq_str`, `ultrafilterBasis_is_basis`, `Profinite.projective_ultrafilter`, `instTotallyDisconnectedSpaceUltrafilter`, `isProperMap_iff_isClosedMap_ultrafilter`, `ultrafilter_isOpen_basic`, `Ultrafilter.pure_injective`, `Set.Finite.notMem_hyperfilter`, `Ultrafilter.eq_pure_of_finite`, `Compactum.continuous_of_hom`, `Ultrafilter.compl_notMem_iff`, `mem_closure_iff_ultrafilter`, `isDenseInducing_pure`, `Ultrafilter.tendsto_pure_self`, `Ultrafilter.t2Space`, `continuous_ultrafilter_extend`, `Ultrafilter.lawfulMonad`, `Compactum.str_hom_commute`, `CompHaus.projective_ultrafilter`, `Filter.compl_mem_hyperfilter_of_finite`, `Ultrafilter.compl_mem_iff_notMem`, `Ultrafilter.coe_injective`, `Ultrafilter.mem_coe`, `OnePoint.ultrafilter_le_nhds_infty`, `ultrafilter_isClosed_basic`, `ultrafilter_converges_iff`, `Ultrafilter.empty_notMem`, `Ultrafilter.le_cofinite_or_eq_pure`, `Ultrafilter.finite_sUnion_mem_iff`, `ultrafilter_comap_pure_nhds`, `Ultrafilter.instNonempty`, `Ultrafilter.ext_iff`, `Ultrafilter.continuous_mul_left`, `Filter.mem_hyperfilter_of_finite_compl`, `Compactum.isClosed_iff`, `Ultrafilter.eventually_add`, `Compactum.isClosed_cl`, `ultrafilter_extend_pure`, `Compactum.join_distrib`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt_iff_ultrafilter` 📖	mathematical	—	`ClusterPt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds`	—	`inf_comm`
`continuousAt_iff_ultrafilter` 📖	mathematical	—	`ContinuousAt` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	—	`Filter.tendsto_iff_ultrafilter`
`continuous_iff_ultrafilter` 📖	mathematical	—	`Continuous` `Filter.Tendsto` `Ultrafilter.toFilter` `nhds`	—	—
`isClosed_iff_ultrafilter` 📖	mathematical	—	`IsClosed` `Set` `Set.instMembership`	—	—
`isOpen_iff_ultrafilter` 📖	mathematical	—	`IsOpen` `Set` `Ultrafilter` `Ultrafilter.instMembershipSet`	—	—
`mapClusterPt_iff_ultrafilter` 📖	mathematical	—	`MapClusterPt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `Filter.Tendsto` `nhds`	—	`inf_comm`
`mem_closure_iff_ultrafilter` 📖	mathematical	—	`Set` `Set.instMembership` `closure` `Ultrafilter` `Ultrafilter.instMembershipSet` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds`	—	`closure_eq_cluster_pts`

---

← Back to Index