Theorems · Theorem · global analysis
ModelWithCorners.source_eq
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (self : ModelWithCorners 𝕜 E H),
self.source = Set.univ- Cited by
- 34 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Set.univstatement · cited by 3,945
- ModelWithCornersstatement and proof · cited by 2,462
- PartialEquiv.sourcestatement · cited by 964
- ModelWithCorners.toPartialEquivstatement · cited by 72
Cited by34
Results whose statement or proof uses this declaration.
- ModelWithCorners.left_invproof · cited by 56
- ModelWithCorners.target_eqproof · cited by 42
- OpenPartialHomeomorph.extend_sourceproof · cited by 17
- ContMDiffWithinAt.mdifferentiableWithinAtproof · cited by 11
- ModelWithCorners.image_eqproof · cited by 11
- HasMFDerivWithinAt.compproof · cited by 7
- contMDiff_iffproof · cited by 4
- preimage_extChartAt_eventuallyEq_compl_singletonproof · cited by 3
- ContMDiffWithinAt.mfderivWithinproof · cited by 3
- mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'proof · cited by 3
- VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symmproof · cited by 2
- contMDiff_equivTangentBundleProd_symmproof · cited by 2