Documentation Verification Report

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.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	2 math math: `id_mem`, `mem_groupoid_of_pregroupoid`

Theorems

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

StructureGroupoid

Definitions

Name	Category	Theorems
`members` 📖	CompOp	1 math math: `id_mem'`
`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` 📖	—	`IsOpen` `Set` `Set.instMembership` `OpenPartialHomeomorph` `StructureGroupoid` `instMembershipOpenPartialHomeomorphStructureGroupoid` `OpenPartialHomeomorph.restr`	—	—	`locality'`
`locality'` 📖	—	`IsOpen` `Set` `Set.instMembership` `OpenPartialHomeomorph` `members` `OpenPartialHomeomorph.restr`	—	—	—
`mem_iff_of_eqOnSource` 📖	mathematical	`OpenPartialHomeomorph` `OpenPartialHomeomorph.eqOnSourceSetoid`	`StructureGroupoid` `instMembershipOpenPartialHomeomorphStructureGroupoid`	—	`mem_of_eqOnSource`
`mem_of_eqOnSource` 📖	—	`OpenPartialHomeomorph` `StructureGroupoid` `instMembershipOpenPartialHomeomorphStructureGroupoid` `OpenPartialHomeomorph.eqOnSourceSetoid`	—	—	`mem_of_eqOnSource'`
`mem_of_eqOnSource'` 📖	—	`OpenPartialHomeomorph` `Set` `Set.instMembership` `members` `OpenPartialHomeomorph.eqOnSourceSetoid`	—	—	—
`symm'` 📖	mathematical	`OpenPartialHomeomorph` `Set` `Set.instMembership` `members`	`OpenPartialHomeomorph.symm`	—	—
`trans` 📖	mathematical	`OpenPartialHomeomorph` `StructureGroupoid` `instMembershipOpenPartialHomeomorphStructureGroupoid`	`OpenPartialHomeomorph.trans`	—	`trans'`
`trans'` 📖	mathematical	`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	24 math math: `StructureGroupoid.mem_iff_of_eqOnSource`, `contDiffGroupoid_le`, `OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff`, `OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff`, `hasGroupoid_inf_iff`, `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'`, `ofSet_mem_contDiffGroupoid`, `Structomorph.mem_groupoid`, `ContinuousGroupoid.mem_of_source_eq_empty`, `StructureGroupoid.id_mem`, `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	20 math math: `StructureGroupoid.mem_iff_of_eqOnSource`, `OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff`, `OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff`, `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'`, `ofSet_mem_contDiffGroupoid`, `Structomorph.mem_groupoid`, `ContinuousGroupoid.mem_of_source_eq_empty`, `StructureGroupoid.id_mem`, `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.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` 📖	—	`OpenPartialHomeomorph` `OpenPartialHomeomorph.eqOnSourceSetoid` `Pregroupoid.property` `OpenPartialHomeomorph.toFun'` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	—	—	`Pregroupoid.congr` `OpenPartialHomeomorph.open_source` `Set.EqOn.symm` `OpenPartialHomeomorph.EqOnSource.eqOn`

---

← Back to Index