Profinite

📁 Source: Mathlib/Topology/Separation/Profinite.lean

Statistics

Metric	Count
Definitions Profinite	1
Theorems compact_exists_isClopen_in_isOpen, exists_clopen_of_closed_subset_open, exists_clopen_partition_of_clopen_cover, instTotallySeparatedSpaceOfTotallyDisconnectedSpace, isTopologicalBasis_isClopen, loc_compact_Haus_tot_disc_of_zero_dim, loc_compact_t2_tot_disc_iff_tot_sep, nhds_basis_clopen, totallySeparatedSpace_of_t0_of_basis_clopen, totallySeparatedSpace_of_t1_of_basis_clopen	10
Total	11

(root)

Definitions

Name	Category	Theorems
Profinite 📖	CompOp	85 math math: ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.Extend.cocone_pt, CondensedMod.IsSolid.isIso_solidification_map, Profinite.forget_preservesLimits, instFullFintypeCatProfiniteToProfinite, Profinite.Extend.functorOp_map, Profinite.instEnoughProjectives, CondensedMod.isDiscrete_tfae, Profinite.Extend.cone_π_app, Profinite.effectiveEpi_tfae, instFaithfulLightDiagramProfiniteLightDiagramToProfinite, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, lightDiagramToProfinite_map, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.lanPresheafExt_inv, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instFaithfulFintypeCatProfiniteToProfinite, Profinite.injective_of_light, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.epi_iff_surjective, lightProfiniteToLightDiagram_map, Profinite.exists_locallyConstant_finite_aux, lightDiagramToLightProfinite_obj, Profinite.isIso_indexCone_lift, Condensed.isoFinYonedaComponents_hom_apply, Profinite.Extend.functorOp_obj, Condensed.finYoneda_map, LightProfinite.lightToProfinite_map_proj_eq, FintypeCat.toProfinite_map_hom_hom_apply, Profinite.hasColimits, Profinite.instPreregular, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instCountableDiscreteQuotient, Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone, Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus, Profinite.projective_ultrafilter, CompHaus.toProfinite_obj', Condensed.isoLocallyConstantOfIsColimit_inv, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, lightDiagramToProfinite_obj, Condensed.lanPresheafNatIso_hom_app, Profinite.Extend.functor_obj, Condensed.isoFinYonedaComponents_inv_comp, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, Profinite.lift_lifts_assoc, CondensedSet.isDiscrete_tfae, Profinite.exists_locallyConstant, Profinite.lift_lifts, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite, LightDiagram.id_hom_hom_hom_apply, Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Profinite.Extend.cocone_ι_app, Condensed.isoFinYoneda_hom_app, Profinite.Extend.cone_pt, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, Profinite.projective_of_extrDisc, Condensed.lanPresheafExt_hom, instFullLightDiagramProfiniteLightDiagramToProfinite, Profinite.injective_of_finite, Stonean.instProjectiveProfiniteObjToProfinite, LightDiagram.comp_hom_hom_hom_apply, Profinite.presentation.epi_π, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, Profinite.exists_locallyConstant_finite_nonempty, Profinite.hasLimits, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.isoFinYoneda_inv_app, Profinite.exists_locallyConstant_fin_two, Profinite.effectiveEpiFamily_tfae, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, Profinite.Extend.functor_map, Condensed.locallyConstantIsoFinYoneda_hom_app, Condensed.equalizerCondition_profinite, Profinite.isIso_asLimitCone_lift, Condensed.lanPresheafIso_hom, Profinite.exists_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compact_exists_isClopen_in_isOpen 📖	mathematical	IsOpen Set Set.instMembership	IsClopen Set.instHasSubset	—	TopologicalSpace.IsTopologicalBasis.mem_nhds_iff isTopologicalBasis_isClopen IsOpen.mem_nhds
exists_clopen_of_closed_subset_open 📖	mathematical	IsOpen Set Set.instHasSubset	IsClopen	—	Set.mem_iUnion Set.Finite.isClopen_biUnion Finset.finite_toSet Set.iUnion_coe_set IsCompact.elim_finite_subcover IsClosed.isCompact IsClopen.isOpen compact_exists_isClopen_in_isOpen
exists_clopen_partition_of_clopen_cover 📖	mathematical	IsClosed IsClopen Set Set.instHasSubset Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ	Set.iUnion	—	Finite.induction_empty_option Set.InjOn.pairwiseDisjoint_image Function.Injective.injOn Equiv.injective Set.image_univ EquivLike.range_eq_univ Equiv.apply_symm_apply Function.Surjective.iUnion_comp Equiv.surjective PEmpty.instIsEmpty Set.iUnion_of_empty Set.instReflSubset Option.some_injective Set.PairwiseDisjoint.subset IsOpen.sdiff isClosed_iUnion_of_finite Finite.of_fintype Set.subset_diff exists_clopen_of_closed_subset_open subset_trans Set.instIsTransSubset Set.diff_subset IsClopen.diff Disjoint.mono_right Disjoint.mono_left Set.subset_iUnion_of_subset isClopen_iUnion_of_finite Set.mem_iUnion Set.pairwiseDisjoint_iff Set.inter_self Set.subset_iUnion Set.disjoint_sdiff_left Set.disjoint_sdiff_right
instTotallySeparatedSpaceOfTotallyDisconnectedSpace 📖	mathematical	—	TotallySeparatedSpace	—	loc_compact_t2_tot_disc_iff_tot_sep
isTopologicalBasis_isClopen 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis setOf Set IsClopen	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds IsOpen.mem_nhds Filter.HasBasis.mem_iff nhds_basis_clopen
loc_compact_Haus_tot_disc_of_zero_dim 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis setOf Set IsClopen	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds exists_compact_subset IsOpen.preimage continuous_subtype_val isOpen_interior CanLift.prf Subtype.canLift interior_subset compact_exists_isClopen_in_isOpen instT2SpaceSubtype isCompact_iff_compactSpace Subtype.totallyDisconnectedSpace Topology.IsClosedEmbedding.isClosed_iff_image_isClosed IsClosed.isClosedEmbedding_subtypeVal IsCompact.isClosed Topology.IsEmbedding.comp Topology.IsEmbedding.subtypeVal Set.range_comp Subtype.range_coe Subtype.image_preimage_coe Set.inter_eq_self_of_subset_right Set.image_comp Topology.IsOpenEmbedding.isOpenMap Subtype.coe_eta Set.Subset.trans Subtype.coe_preimage_self
loc_compact_t2_tot_disc_iff_tot_sep 📖	mathematical	—	TotallyDisconnectedSpace TotallySeparatedSpace	—	totallySeparatedSpace_of_t0_of_basis_clopen T1Space.t0Space T2Space.t1Space loc_compact_Haus_tot_disc_of_zero_dim TotallySeparatedSpace.totallyDisconnectedSpace
nhds_basis_clopen 📖	mathematical	—	Filter.HasBasis Set nhds Set.instMembership IsClopen	—	totallyDisconnectedSpace_iff_connectedComponent_singleton IsClopen.inter Set.inter_subset_left Set.inter_subset_right Set.mem_singleton_iff connectedComponent_eq_iInter_isClopen exists_subset_nhds_of_compactSpace isClopen_univ Set.mem_univ mem_nhds_iff
totallySeparatedSpace_of_t0_of_basis_clopen 📖	mathematical	TopologicalSpace.IsTopologicalBasis setOf Set IsClopen	TotallySeparatedSpace	—	IsClopen.isOpen IsClopen.compl Set.notMem_subset Eq.superset Set.instReflSubset Set.union_compl_self disjoint_compl_right TopologicalSpace.IsTopologicalBasis.isOpen_iff Set.union_comm disjoint_compl_left exists_isOpen_xor'_mem
totallySeparatedSpace_of_t1_of_basis_clopen 📖	mathematical	TopologicalSpace.IsTopologicalBasis setOf Set IsClopen	TotallySeparatedSpace	—	totallySeparatedSpace_of_t0_of_basis_clopen

---

← Back to Index