Theorem StructureGroupoid.mem_iff_of_eqOnSource

Modification history

2026-01-15 09:15
Mathlib/Geometry/Manifold/ChartedSpace.lean
refactor(Geometry/Manifold): split long file ChartedSpace.lean (#33896) …
Modified StructureGroupoid.mem_iff_of_eqOnSourceView on Github →
2024-05-21 20:03
Mathlib/Geometry/Manifold/ChartedSpace.lean
feat(StructureGroupoid): one small lemma and some docstrings (#9827) …
Added StructureGroupoid.mem_iff_of_eqOnSourceView on Github →