internlm/Lean-Github huggingface dataset:
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
h₂s : MeasureZero I s
h : ¬s = ∅
x : M
hx : x ∈ s
this : (chartAt H x).source ∩ s = ∅
⊢ x ∈ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
have : Set.Nonempty (I ∘ e '' (e.source ∩ s)) := (Iff.mp Set.nmem_singleton_empty h).image _
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
have : IsOpen (I ∘ e '' (e.source ∩ s)) := by
  rw [Set.image_comp]
  exact I.toHomeomorph.isOpenMap _ (e.isOpen_image_source_inter h₁s)
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this✝ : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
this : IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this✝ : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
this : IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
⊢ (interior (↑I ∘ ↑e '' (e.source ∩ s))).Nonempty
Tactic:
rwa [this.interior_eq]
Proof state after:
no goals
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I ∘ ↑e '' (e.source ∩ s))
Tactic:
rw [Set.image_comp]
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I '' (↑e '' (e.source ∩ s)))
Theorem: MeasureZero.open_implies_empty
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✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set M
h₁s : IsOpen s
x : M
e : PartialHomeomorph M H := chartAt H x
K'' : PositiveCompacts E
μ : Measure E := addHaarMeasure K''
h₂s : ↑μ (↑I ∘ ↑(chartAt H x) '' ((chartAt H x).source ∩ s)) = 0
h : ¬(chartAt H x).source ∩ s = ∅
this : (↑I ∘ ↑e '' (e.source ∩ s)).Nonempty
⊢ IsOpen (↑I '' (↑e '' (e.source ∩ s)))
Tactic:
exact I.toHomeomorph.isOpenMap _ (e.isOpen_image_source_inter h₁s)
Proof state after:
no goals
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
⊢ MeasureZero J (f '' s)
Tactic:
let U : M → Set M := fun x ↦ (ChartedSpace.chartAt x : PartialHomeomorph M H).source
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ MeasureZero J (f '' s)
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ MeasureZero J (f '' s)
Tactic:
have hcovering : univ ⊆ ⋃ (x : M), U x := by
  intro x _
  rw [mem_iUnion]
  exact ⟨x, mem_chart_source H x⟩
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
⊢ MeasureZero J (f '' s)
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
⊢ MeasureZero J (f '' s)
Tactic:
have hopen : ∀ x : M, IsOpen (U x) := fun x => (ChartedSpace.chartAt x).open_source
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
⊢ MeasureZero J (f '' s)
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
⊢ MeasureZero J (f '' s)
Tactic:
let ⟨T, ⟨hTCountable, hTcover⟩⟩ := TopologicalSpace.isOpen_iUnion_countable U hopen
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
⊢ MeasureZero J (f '' s)
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
⊢ MeasureZero J (f '' s)
Tactic:
have : ∀ i : T, MeasureZero J (f '' ((U i) ∩ s)) := by
  intro i
  let e : PartialHomeomorph M H := ChartedSpace.chartAt i
  have h : MeasureZero J (f '' (e.source ∩ s)) := hs i
  have h₃ : U i = e.source := by rw [← Filter.principal_eq_iff_eq]
  apply h.mono _
  apply image_subset
  rw [h₃]
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ MeasureZero J (f '' s)
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (f '' s)
Tactic:
rw [← decomp]
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✝²⁰ : FiniteDimensional ℝ E✝
inst✝¹⁹ : MeasurableSpace E✝
inst✝¹⁸ : BorelSpace E✝
E : Type u_4
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
H : Type u_5
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_6
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
inst✝¹² : SmoothManifoldWithCorners I M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : SecondCountableTopology M
F : Type u_7
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
G : Type u_8
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_9
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
inst✝⁴ : J.Boundaryless
inst✝³ : SmoothManifoldWithCorners J N
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : M → N
s : Set M
hs : ∀ (x : M), MeasureZero J (f '' ((chartAt H x).source ∩ s))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
hcovering : univ ⊆ ⋃ x, U x
hopen : ∀ (x : M), IsOpen (U x)
T : Set M
hTCountable : T.Countable
hTcover : ⋃ i ∈ T, U i = ⋃ i, U i
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ s))