HasGroupoid

📁 Source: Mathlib/Geometry/Manifold/HasGroupoid.lean

Statistics

Metric	Count
Definitions HasGroupoid, singletonChartedSpace, toStructomorph, Structomorph, refl, toHomeomorph, trans, maximalAtlas, instChartedSpace, singletonChartedSpace	10
Theorems compatible, singletonChartedSpace_chartAt_eq, singletonChartedSpace_chartAt_source, singletonChartedSpace_mem_atlas_eq, singleton_hasGroupoid, mem_groupoid, chart_mem_maximalAtlas, compatible, compatible_of_mem_maximalAtlas, id_mem_maximalAtlas, maximalAtlas_mono, mem_maximalAtlas_of_eqOnSource, mem_maximalAtlas_of_mem_groupoid, restriction_in_maximalAtlas, restriction_mem_maximalAtlas_subtype, subset_maximalAtlas, subtypeRestr_mem_maximalAtlas, trans_restricted, chartAt_eq, chartAt_inclusion_symm_eventuallyEq, chartAt_subtype_val_symm_eventuallyEq, chart_eq, chart_eq', instHasGroupoid, singletonChartedSpace_chartAt_eq, singleton_hasGroupoid, hasGroupoid_continuousGroupoid, hasGroupoid_inf_iff, hasGroupoid_model_space, hasGroupoid_of_le, hasGroupoid_of_pregroupoid, mem_maximalAtlas_iff, restr_mem_maximalAtlas	33
Total	43

HasGroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compatible 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	—

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
singletonChartedSpace 📖	CompOp	4 math math: isManifold_singleton, singletonChartedSpace_chartAt_eq, singleton_hasGroupoid, singletonChartedSpace_chartAt_source
toStructomorph 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singletonChartedSpace_chartAt_eq 📖	mathematical	PartialEquiv.source toPartialEquiv Set.univ	chartAt singletonChartedSpace	—	—
singletonChartedSpace_chartAt_source 📖	mathematical	PartialEquiv.source toPartialEquiv Set.univ	chartAt singletonChartedSpace	—	—
singletonChartedSpace_mem_atlas_eq 📖	—	PartialEquiv.source toPartialEquiv Set.univ OpenPartialHomeomorph Set Set.instMembership ChartedSpace.atlas singletonChartedSpace	—	—	—
singleton_hasGroupoid 📖	mathematical	PartialEquiv.source toPartialEquiv Set.univ	HasGroupoid singletonChartedSpace	—	singletonChartedSpace_mem_atlas_eq StructureGroupoid.mem_of_eqOnSource open_target closedUnderRestriction_iff_id_le StructureGroupoid.le_iff idRestrGroupoid_mem symm_trans_self

Structomorph

Definitions

Name	Category	Theorems
refl 📖	CompOp	—
toHomeomorph 📖	CompOp	1 math math: mem_groupoid
trans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_groupoid 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm Homeomorph.toOpenPartialHomeomorph toHomeomorph	—	—

StructureGroupoid

Definitions

Name	Category	Theorems
maximalAtlas 📖	CompOp	10 math math: mem_maximalAtlas_of_mem_groupoid, chart_mem_maximalAtlas, IsManifold.mem_maximalAtlas_iff, subset_maximalAtlas, restriction_in_maximalAtlas, subtypeRestr_mem_maximalAtlas, id_mem_maximalAtlas, restriction_mem_maximalAtlas_subtype, maximalAtlas_mono, mem_maximalAtlas_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership maximalAtlas chartAt	—	subset_maximalAtlas chart_mem_atlas
compatible 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	HasGroupoid.compatible
compatible_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership maximalAtlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	locality ContinuousOn.isOpen_inter_preimage OpenPartialHomeomorph.continuousOn_toFun OpenPartialHomeomorph.open_source Set.mem_inter_iff mem_maximalAtlas_iff chart_mem_atlas trans IsPreorder.toIsTrans IsEquiv.toIsPreorder Quotient.instIsEquivEquiv OpenPartialHomeomorph.trans_assoc OpenPartialHomeomorph.EqOnSource.trans' refl IsPreorder.toRefl OpenPartialHomeomorph.self_trans_symm OpenPartialHomeomorph.trans_of_set' OpenPartialHomeomorph.restr_trans mem_of_eqOnSource
id_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership maximalAtlas chartedSpaceSelf OpenPartialHomeomorph.refl	—	subset_maximalAtlas hasGroupoid_model_space
maximalAtlas_mono 📖	mathematical	StructureGroupoid Preorder.toLE PartialOrder.toPreorder partialOrder	Set OpenPartialHomeomorph Set.instHasSubset maximalAtlas	—	—
mem_maximalAtlas_of_eqOnSource 📖	—	OpenPartialHomeomorph OpenPartialHomeomorph.eqOnSourceSetoid Set Set.instMembership maximalAtlas	—	—	mem_maximalAtlas_iff mem_of_eqOnSource OpenPartialHomeomorph.EqOnSource.trans' OpenPartialHomeomorph.EqOnSource.symm' OpenPartialHomeomorph.eqOnSource_refl
mem_maximalAtlas_of_mem_groupoid 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	Set Set.instMembership maximalAtlas chartedSpaceSelf	—	trans symm id_mem
restriction_in_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype maximalAtlas TopologicalSpace.Opens.instChartedSpace OpenPartialHomeomorph.subtypeRestr	—	subtypeRestr_mem_maximalAtlas
restriction_mem_maximalAtlas_subtype 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	Set.Elem PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike OpenPartialHomeomorph.open_source maximalAtlas TopologicalSpace.Opens.instChartedSpace OpenPartialHomeomorph.trans PartialEquiv.target Homeomorph.toOpenPartialHomeomorph OpenPartialHomeomorph.toHomeomorphSourceTarget	—	OpenPartialHomeomorph.open_source OpenPartialHomeomorph.open_target Set.nonempty_coe_sort Set.MapsTo.nonempty OpenPartialHomeomorph.mapsTo TopologicalSpace.Opens.chart_eq chartAt_self_eq OpenPartialHomeomorph.subtypeRestr_def OpenPartialHomeomorph.trans_refl OpenPartialHomeomorph.eqOnSource_iff Set.inter_self OpenPartialHomeomorph.subtypeRestr_source Subtype.coe_preimage_self mem_maximalAtlas_of_eqOnSource subtypeRestr_mem_maximalAtlas
subset_maximalAtlas 📖	mathematical	—	Set OpenPartialHomeomorph Set.instHasSubset atlas maximalAtlas	—	compatible
subtypeRestr_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype maximalAtlas TopologicalSpace.Opens.instChartedSpace OpenPartialHomeomorph.subtypeRestr	—	TopologicalSpace.Opens.chart_eq trans_restricted chart_mem_atlas
trans_restricted 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership atlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype OpenPartialHomeomorph.symm OpenPartialHomeomorph.subtypeRestr	—	mem_of_eqOnSource closedUnderRestriction' compatible OpenPartialHomeomorph.isOpen_inter_preimage_symm TopologicalSpace.Opens.is_open' OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
instChartedSpace 📖	CompOp	32 math math: ModelWithCorners.interior_open, instIsManifoldSubtypeMem, chartAt_eq, chartAt_subtype_val_symm_eventuallyEq, contMDiff_inclusion, Manifold.IsImmersionAtOfComplement.ofOpen, Manifold.IsImmersion.of_opens, ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_val, ModelWithCorners.boundary_open, chartAt_inclusion_symm_eventuallyEq, instHasGroupoid, Manifold.IsImmersionAt.of_opens, StructureGroupoid.LocalInvariantProp.liftProp_subtype_val, StructureGroupoid.LocalInvariantProp.section_spec, smoothSheaf.obj_eq, Manifold.IsImmersionOfComplement.ofOpen, ModelWithCorners.BoundarylessManifold.open, Manifold.IsImmersionAtOfComplement.of_opens, StructureGroupoid.LocalInvariantProp.liftProp_inclusion, StructureGroupoid.restriction_in_maximalAtlas, contMDiffAt_subtype_iff, ModelWithCorners.isBoundaryPoint_iff_isBoundaryPoint_val, Manifold.IsImmersion.ofOpen, smoothSheaf.contMDiff_section, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val, Manifold.IsImmersionAt.ofOpen, Manifold.IsImmersionOfComplement.of_opens, StructureGroupoid.subtypeRestr_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion, Manifold.IsSmoothEmbedding.of_opens, StructureGroupoid.restriction_mem_maximalAtlas_subtype, contMDiff_subtype_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chartAt_eq 📖	mathematical	—	chartAt TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype instChartedSpace OpenPartialHomeomorph.subtypeRestr	—	—
chartAt_inclusion_symm_eventuallyEq 📖	mathematical	TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder instPartialOrder	Filter.EventuallyEq SetLike.instMembership instSetLike nhds OpenPartialHomeomorph.toFun' instTopologicalSpaceSubtype chartAt instChartedSpace inclusion Set.inclusion SetLike.coe OpenPartialHomeomorph.symm	—	IsOpen.mem_nhds OpenPartialHomeomorph.open_target OpenPartialHomeomorph.map_subtype_source mem_chart_source Filter.eventuallyEq_of_mem OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le
chartAt_subtype_val_symm_eventuallyEq 📖	mathematical	—	Filter.EventuallyEq nhds OpenPartialHomeomorph.toFun' chartAt TopologicalSpace.Opens SetLike.instMembership instSetLike OpenPartialHomeomorph.symm instTopologicalSpaceSubtype instChartedSpace	—	IsOpen.mem_nhds OpenPartialHomeomorph.open_target OpenPartialHomeomorph.map_subtype_source mem_chart_source Filter.eventuallyEq_of_mem OpenPartialHomeomorph.subtypeRestr_symm_eqOn
chart_eq 📖	mathematical	OpenPartialHomeomorph TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype Set Set.instMembership atlas instChartedSpace	OpenPartialHomeomorph.subtypeRestr chartAt	—	Set.mem_singleton_iff
chart_eq' 📖	mathematical	OpenPartialHomeomorph TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype Set Set.instMembership atlas instChartedSpace chartedSpaceSelf	OpenPartialHomeomorph.subtypeRestr chartAt	—	chart_eq
instHasGroupoid 📖	mathematical	—	HasGroupoid TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype instChartedSpace	—	Set.mem_singleton_iff StructureGroupoid.mem_of_eqOnSource closedUnderRestriction' StructureGroupoid.compatible chart_mem_atlas OpenPartialHomeomorph.isOpen_inter_preimage_symm is_open' OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr

Topology.IsOpenEmbedding

Definitions

Name	Category	Theorems
singletonChartedSpace 📖	CompOp	6 math math: ContMDiff.of_comp_isOpenEmbedding, contMDiffOn_isOpenEmbedding_symm, contMDiff_isOpenEmbedding, singleton_hasGroupoid, isManifold_singleton, singletonChartedSpace_chartAt_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singletonChartedSpace_chartAt_eq 📖	mathematical	Topology.IsOpenEmbedding	OpenPartialHomeomorph.toFun' chartAt singletonChartedSpace	—	—
singleton_hasGroupoid 📖	mathematical	Topology.IsOpenEmbedding	HasGroupoid singletonChartedSpace	—	OpenPartialHomeomorph.singleton_hasGroupoid toOpenPartialHomeomorph_source

(root)

Definitions

Name	Category	Theorems
HasGroupoid 📖	CompData	12 math math: hasGroupoid_of_le, hasGroupoid_inf_iff, TopologicalSpace.Opens.instHasGroupoid, IsManifold.toHasGroupoid, Topology.IsOpenEmbedding.singleton_hasGroupoid, ContMDiffFiberwiseLinear.hasGroupoid, TopCat.of.hasGroupoid, StructureGroupoid.HasGroupoid.comp, hasGroupoid_continuousGroupoid, hasGroupoid_model_space, OpenPartialHomeomorph.singleton_hasGroupoid, hasGroupoid_of_pregroupoid
Structomorph 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGroupoid_continuousGroupoid 📖	mathematical	—	HasGroupoid continuousGroupoid	—	continuousGroupoid.eq_1 mem_groupoid_of_pregroupoid
hasGroupoid_inf_iff 📖	mathematical	—	HasGroupoid StructureGroupoid instMinStructureGroupoid	—	hasGroupoid_of_le inf_le_left inf_le_right HasGroupoid.compatible
hasGroupoid_model_space 📖	mathematical	—	HasGroupoid chartedSpaceSelf	—	chartedSpaceSelf_atlas OpenPartialHomeomorph.trans_refl
hasGroupoid_of_le 📖	mathematical	StructureGroupoid Preorder.toLE PartialOrder.toPreorder StructureGroupoid.partialOrder	HasGroupoid	—	HasGroupoid.compatible
hasGroupoid_of_pregroupoid 📖	mathematical	Pregroupoid.property OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	HasGroupoid Pregroupoid.groupoid	—	mem_groupoid_of_pregroupoid
mem_maximalAtlas_iff 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	—
restr_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas IsOpen	OpenPartialHomeomorph.restr	—	—

---

← Back to Index