Theorems · Theorem · manifolds
mem_chart_source
∀ (H : Type u_5) {M : Type u_6} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
(x : M), x ∈ (chartAt H x).source- Defined in
- Mathlib.Geometry.Manifold.ChartedSpace
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- ChartedSpacestatement and proof · cited by 2,397
- PartialEquiv.sourcestatement · cited by 964
- PartialHomeomorph.toPartialEquivstatement · cited by 917
- OpenPartialHomeomorph.toPartialHomeomorphstatement · cited by 851
- chartAtstatement · cited by 301
- ChartedSpace.mem_chart_sourceproof · cited by 2
Cited by39
Results whose statement or proof uses this declaration.
- tangentBundleCoreproof · cited by 25
- chart_source_mem_nhdsproof · cited by 9
- mem_chart_targetproof · cited by 5
- ChartedSpace.locallyCompactSpaceproof · cited by 5
- ContMDiff.inlproof · cited by 3
- ContMDiff.inrproof · cited by 3
- StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter'proof · cited by 3
- isImmersionOfComplement_subtypeVal_Iccproof · cited by 3
- ModelWithCorners.isInteriorPoint_iff_isInteriorPoint_valproof · cited by 2
- ModelWithCorners.isInteriorPoint_iff_of_mem_atlasproof · cited by 2
- Manifold.IsImmersionAtOfComplement.of_opensproof · cited by 2