Theorems · Theorem · manifolds
chart_source_mem_nhds
∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
(x : M), (chartAt H x).source ∈ nhds x- Defined in
- Mathlib.Geometry.Manifold.ChartedSpace
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- ChartedSpacestatement and proof · cited by 2,397
- PartialEquiv.sourcestatement · cited by 964
- PartialHomeomorph.toPartialEquivstatement · cited by 917
- OpenPartialHomeomorph.toPartialHomeomorphstatement · cited by 851
- IsOpen.mem_nhdsproof · cited by 470
- chartAtstatement and proof · cited by 301
- OpenPartialHomeomorph.open_sourceproof · cited by 65
- mem_chart_sourceproof · cited by 38
Cited by9
Results whose statement or proof uses this declaration.
- ContMDiffWithinAt.mlieBracketWithin_vectorFieldproof · cited by 3
- contMDiff_equivTangentBundleProd_symmproof · cited by 2
- StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iffproof · cited by 2
- ChartedSpace.secondCountable_of_sigmaCompactproof · cited by 2
- eventually_norm_mfderivWithin_symm_extChartAt_comp_ltproof · cited by 1
- VectorField.leibniz_identity_mlieBracketWithin_applyproof · cited by 1
- eventually_norm_mfderiv_extChartAt_ltproof · cited by 1
- eventually_riemannianEDist_le_edist_extChartAtproof · cited by 1
- ChartedSpace.locallyPathConnectedSpaceproof · cited by 1