internlm/Lean-Github huggingface dataset:
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
⊢ ↑ν (g '' U) = 0
Tactic:
have aux : μ' (incl '' U) = 0 := by sorry
Proof state after:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Tactic:
have : ν ((pi ∘ g' ∘ incl) '' U) = 0 := by
  sorry
Proof state after:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (g '' U) = 0
Tactic:
rw [← commutes]
Proof state after:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 0
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case intro
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
this : ↑ν (pi ∘ g' ∘ incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 0
Tactic:
exact this
Proof state after:
no goals
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
⊢ pi ∘ g' ∘ incl = g
Tactic:
ext y
Proof state after:
case h
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
y : E
⊢ (pi ∘ g' ∘ incl) y = g y
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
case h
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
y : E
⊢ (pi ∘ g' ∘ incl) y = g y
Tactic:
rw [comp_apply, comp_apply]
Proof state after:
no goals
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
⊢ ↑μ' (incl '' U) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: image_measure_zero_of_C1_dimension_increase
Proof state before:
E : Type u_1
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace ℝ E
H : Type u_2
inst✝²¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝²⁰ : TopologicalSpace M
inst✝¹⁹ : ChartedSpace H M
inst✝¹⁸ : I.Boundaryless
inst✝¹⁷ : SmoothManifoldWithCorners I M
inst✝¹⁶ : FiniteDimensional ℝ E
inst✝¹⁵ : SecondCountableTopology M
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace E
F : Type u_4
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace ℝ F
G : Type u_5
inst✝¹⁰ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁹ : TopologicalSpace N
inst✝⁸ : ChartedSpace G N
inst✝⁷ : J.Boundaryless
inst✝⁶ : SmoothManifoldWithCorners J N
inst✝⁵ : FiniteDimensional ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
g : E → F
U : Set E
hU : IsOpen U
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hg : ContDiffOn ℝ 1 g U
hmn : m < n
incl : E → E × (Fin (n - m) → ℝ) := fun x => (x, 0)
g' : E × (Fin (n - m) → ℝ) → F × (Fin (n - m) → ℝ) :=
  fun x =>
    match x with
    | (y, snd) => (g y, 0)
pi : F × (Fin (n - m) → ℝ) → F :=
  fun x =>
    match x with
    | (f, snd) => f
commutes : pi ∘ g' ∘ incl = g
K'' : PositiveCompacts (E × (Fin (n - m) → ℝ))
μ' : Measure (E × (Fin (n - m) → ℝ)) := addHaarMeasure K''
aux : ↑μ' (incl '' U) = 0
⊢ ↑ν (pi ∘ g' ∘ incl '' U) = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
⊢ MeasureZero J (range f)
Tactic:
rw [← image_univ]
Proof state after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
⊢ MeasureZero J (f '' univ)
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
⊢ MeasureZero J (f '' univ)
Tactic:
suffices hyp : ∀ x : M, MeasureZero J (f '' ((chartAt H x).source ∩ univ)) from
  measure_zero_image_iff_chart_domains (J := J) hyp
Proof state after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
⊢ ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ univ))
Theorem: image_null_of_C1_of_dimension_increase
Proof state before:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
⊢ ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ univ))
Tactic:
intro x μ hμ y
Proof state after:
E : Type u_1
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁷ : TopologicalSpace M
inst✝¹⁶ : ChartedSpace H M
inst✝¹⁵ : I.Boundaryless
inst✝¹⁴ : SmoothManifoldWithCorners I M
inst✝¹³ : FiniteDimensional ℝ E
inst✝¹² : SecondCountableTopology M
inst✝¹¹ : MeasurableSpace E
inst✝¹⁰ : BorelSpace E
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_5
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : M → N
hf : ContMDiff I J (↑r) f
hdim : m < n
x : M
μ : Measure F
hμ : μ.IsAddHaarMeasure
y : N
⊢ ↑μ (↑J ∘ ↑(chartAt G y) '' ((chartAt G y).source ∩ f '' ((chartAt H x).source ∩ univ))) = 0