Theorems · Theorem · measure theory

ContDiff.dense_compl_range_of_finrank_lt_finrank

∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F},
  ContDiff ℝ 1 f → Module.finrank ℝ E < Module.finrank ℝ F → Dense (Set.range f)ᶜ

A particular case of Sard's Theorem. If f is a C¹ smooth map from a real vector space to a real vector space F of strictly larger dimension, then the complement of the range of f is dense in F.

Defined in: Mathlib.Topology.MetricSpace.HausdorffDimension
Cited by: 0 results in Mathlib
Foundations: Depth 256 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace FiniteDimensional NormedAddCommGroup NormedSpace FiniteDimensional

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
ENatstatement · cited by 4,985
Set.rangestatement · cited by 4,705
WithTopstatement · cited by 3,754
Compl.complstatement · cited by 2,925
FiniteDimensionalstatement and proof · cited by 1,854
Module.finrankstatement and proof · cited by 1,770
LE.le.trans_ltproof · cited by 795
Densestatement · cited by 359

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.