StructureGroupoid

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

Statistics

Metric	Count
Definitions ClosedUnderRestriction, «term_≫_», «term_≫ₕ_», Pregroupoid, groupoid, property, StructureGroupoid, members, partialOrder, continuousGroupoid, continuousPregroupoid, idGroupoid, idRestrGroupoid, instCompleteLatticeStructureGroupoid, instInfSetStructureGroupoid, instInhabitedPregroupoid, instInhabitedStructureGroupoid, instMembershipOpenPartialHomeomorphStructureGroupoid, instMinStructureGroupoid, instSetLikeStructureGroupoidOpenPartialHomeomorph, instStructureGroupoidOrderBot, instStructureGroupoidOrderTop	22
Theorems closedUnderRestriction, comp, id_mem, locality, id_mem, id_mem', le_iff, locality, locality', mem_iff_of_eqOnSource, mem_of_eqOnSource, mem_of_eqOnSource', symm', trans, trans', closedUnderRestriction', closedUnderRestriction_idRestrGroupoid, closedUnderRestriction_iff_id_le, groupoid_of_pregroupoid_le, idRestrGroupoid_mem, instClosedUnderRestrictionContinuousGroupoid, mem_groupoid_of_pregroupoid, mem_pregroupoid_of_eqOnSource	23
Total	45

ClosedUnderRestriction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedUnderRestriction 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid IsOpen	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.restr	—	—

Manifold

Definitions

Name	Category	Theorems
«term_≫_» 📖	CompOp	—
«term_≫ₕ_» 📖	CompOp	—

Pregroupoid

Definitions

Name	Category	Theorems
groupoid 📖	CompOp	3 math math: groupoid_of_pregroupoid_le, hasGroupoid_of_pregroupoid, mem_groupoid_of_pregroupoid
property 📖	MathDef	6 math math: comp, id_mem, congr, locality, mem_pregroupoid_of_eqOnSource, mem_groupoid_of_pregroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	property IsOpen Set Set.instInter Set.preimage	property Set Set.instInter Set.preimage	—	—
id_mem 📖	mathematical	—	property Set.univ	—	—
locality 📖	mathematical	IsOpen Set Set.instMembership property Set.instInter	property	—	—

StructureGroupoid

Definitions

Name	Category	Theorems
members 📖	CompOp	5 math math: id_mem', mem_of_eqOnSource', locality', symm', trans'
partialOrder 📖	CompOp	4 math math: contDiffGroupoid_le, closedUnderRestriction_iff_id_le, le_iff, groupoid_of_pregroupoid_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_mem 📖	mathematical	—	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.refl	—	id_mem'
id_mem' 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership members OpenPartialHomeomorph.refl	—	—
le_iff 📖	mathematical	—	StructureGroupoid Preorder.toLE PartialOrder.toPreorder partialOrder OpenPartialHomeomorph instMembershipOpenPartialHomeomorphStructureGroupoid	—	—
locality 📖	mathematical	Set IsOpen Set.instMembership OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.restr	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	—	locality'
locality' 📖	mathematical	Set IsOpen Set.instMembership OpenPartialHomeomorph members OpenPartialHomeomorph.restr	OpenPartialHomeomorph Set Set.instMembership members	—	—
mem_iff_of_eqOnSource 📖	mathematical	OpenPartialHomeomorph OpenPartialHomeomorph.eqOnSourceSetoid	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	—	mem_of_eqOnSource
mem_of_eqOnSource 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.eqOnSourceSetoid	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	—	mem_of_eqOnSource'
mem_of_eqOnSource' 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership members OpenPartialHomeomorph.eqOnSourceSetoid	OpenPartialHomeomorph Set Set.instMembership members	—	—
symm' 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership members	OpenPartialHomeomorph Set Set.instMembership members OpenPartialHomeomorph.symm	—	—
trans 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.trans	—	trans'
trans' 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership members	OpenPartialHomeomorph Set Set.instMembership members OpenPartialHomeomorph.trans	—	—

(root)

Definitions

Name	Category	Theorems
ClosedUnderRestriction 📖	CompData	4 math math: instClosedUnderRestrictionContDiffGroupoid, closedUnderRestriction_iff_id_le, instClosedUnderRestrictionContinuousGroupoid, closedUnderRestriction_idRestrGroupoid
Pregroupoid 📖	CompData	—
StructureGroupoid 📖	CompData	31 math math: StructureGroupoid.mem_of_eqOnSource, StructureGroupoid.mem_iff_of_eqOnSource, StructureGroupoid.locality, contDiffGroupoid_le, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff, OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff, hasGroupoid_inf_iff, ClosedUnderRestriction.closedUnderRestriction, closedUnderRestriction_iff_id_le, symm_trans_mem_contDiffGroupoid, StructureGroupoid.compatible_of_mem_maximalAtlas, StructureGroupoid.compatible, StructureGroupoid.le_iff, IsManifold.compatible_of_mem_maximalAtlas, groupoid_of_pregroupoid_le, idRestrGroupoid_mem, StructureGroupoid.trans_restricted, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff', StructureGroupoid.trans, ofSet_mem_contDiffGroupoid, Structomorph.mem_groupoid, StructureGroupoid.symm, ContinuousGroupoid.mem_of_source_eq_empty, StructureGroupoid.id_mem, closedUnderRestriction', contDiffGroupoid_prod, ContDiffGroupoid.mem_of_source_eq_empty, mem_contMDiffFiberwiseLinear_iff, HasGroupoid.compatible, mem_maximalAtlas_iff, mem_groupoid_of_pregroupoid
continuousGroupoid 📖	CompOp	4 math math: contDiffGroupoid_zero_eq, instClosedUnderRestrictionContinuousGroupoid, ContinuousGroupoid.mem_of_source_eq_empty, hasGroupoid_continuousGroupoid
continuousPregroupoid 📖	CompOp	—
idGroupoid 📖	CompOp	—
idRestrGroupoid 📖	CompOp	3 math math: closedUnderRestriction_iff_id_le, idRestrGroupoid_mem, closedUnderRestriction_idRestrGroupoid
instCompleteLatticeStructureGroupoid 📖	CompOp	—
instInfSetStructureGroupoid 📖	CompOp	—
instInhabitedPregroupoid 📖	CompOp	—
instInhabitedStructureGroupoid 📖	CompOp	—
instMembershipOpenPartialHomeomorphStructureGroupoid 📖	CompOp	27 math math: StructureGroupoid.mem_of_eqOnSource, StructureGroupoid.mem_iff_of_eqOnSource, StructureGroupoid.locality, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff, OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff, ClosedUnderRestriction.closedUnderRestriction, symm_trans_mem_contDiffGroupoid, StructureGroupoid.compatible_of_mem_maximalAtlas, StructureGroupoid.compatible, StructureGroupoid.le_iff, IsManifold.compatible_of_mem_maximalAtlas, idRestrGroupoid_mem, StructureGroupoid.trans_restricted, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff', StructureGroupoid.trans, ofSet_mem_contDiffGroupoid, Structomorph.mem_groupoid, StructureGroupoid.symm, ContinuousGroupoid.mem_of_source_eq_empty, StructureGroupoid.id_mem, closedUnderRestriction', contDiffGroupoid_prod, ContDiffGroupoid.mem_of_source_eq_empty, mem_contMDiffFiberwiseLinear_iff, HasGroupoid.compatible, mem_maximalAtlas_iff, mem_groupoid_of_pregroupoid
instMinStructureGroupoid 📖	CompOp	1 math math: hasGroupoid_inf_iff
instSetLikeStructureGroupoidOpenPartialHomeomorph 📖	CompOp	—
instStructureGroupoidOrderBot 📖	CompOp	—
instStructureGroupoidOrderTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedUnderRestriction' 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid IsOpen	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid OpenPartialHomeomorph.restr	—	ClosedUnderRestriction.closedUnderRestriction
closedUnderRestriction_idRestrGroupoid 📖	mathematical	—	ClosedUnderRestriction idRestrGroupoid	—	IsOpen.inter OpenPartialHomeomorph.EqOnSource.restr IsOpen.interior_eq
closedUnderRestriction_iff_id_le 📖	mathematical	—	ClosedUnderRestriction StructureGroupoid Preorder.toLE PartialOrder.toPreorder StructureGroupoid.partialOrder idRestrGroupoid	—	StructureGroupoid.le_iff StructureGroupoid.mem_of_eqOnSource OpenPartialHomeomorph.ext Set.ext IsOpen.interior_eq Set.univ_inter closedUnderRestriction' StructureGroupoid.id_mem OpenPartialHomeomorph.ofSet_trans StructureGroupoid.trans idRestrGroupoid_mem
groupoid_of_pregroupoid_le 📖	mathematical	Pregroupoid.property	StructureGroupoid Preorder.toLE PartialOrder.toPreorder StructureGroupoid.partialOrder Pregroupoid.groupoid	—	StructureGroupoid.le_iff mem_groupoid_of_pregroupoid
idRestrGroupoid_mem 📖	mathematical	IsOpen	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid idRestrGroupoid OpenPartialHomeomorph.ofSet	—	refl IsPreorder.toRefl IsEquiv.toIsPreorder Quotient.instIsEquivEquiv
instClosedUnderRestrictionContinuousGroupoid 📖	mathematical	—	ClosedUnderRestriction continuousGroupoid	—	closedUnderRestriction_iff_id_le le_top
mem_groupoid_of_pregroupoid 📖	mathematical	—	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Pregroupoid.groupoid Pregroupoid.property OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv OpenPartialHomeomorph.symm PartialEquiv.target	—	—
mem_pregroupoid_of_eqOnSource 📖	mathematical	OpenPartialHomeomorph OpenPartialHomeomorph.eqOnSourceSetoid Pregroupoid.property OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	Pregroupoid.property OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	Pregroupoid.congr OpenPartialHomeomorph.open_source Set.EqOn.symm OpenPartialHomeomorph.EqOnSource.eqOn

---

← Back to Index