Theorems · Theorem · global analysis

ModelWithCorners.Boundaryless.range_eq_univ

∀ {𝕜 : 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} {I : ModelWithCorners 𝕜 E H}
  [self : I.Boundaryless], Set.range ↑I = Set.univ

Defined in: Mathlib.Geometry.Manifold.IsManifold.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 14 from the axioms · uses no axioms
Assumes: ModelWithCorners.Boundaryless

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

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.rangestatement · cited by 4,705
Set.univstatement · cited by 3,945
ModelWithCornersstatement and proof · cited by 2,462
ModelWithCorners.toFun'statement · cited by 373
ModelWithCorners.Boundarylessstatement and proof · cited by 20

Cited by2

Results whose statement or proof uses this declaration.

ModelWithCorners.range_eq_univproof · cited by 4
Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMaxproof · cited by 1