internlm/Lean-Github huggingface dataset:
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 (⋃ i, f '' (U ↑i ∩ s))
Tactic:
have todo : Encodable T := by sorry
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
todo : Encodable ↑T
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ 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
todo : Encodable ↑T
⊢ MeasureZero J (⋃ i, f '' (U ↑i ∩ s))
Tactic:
apply MeasureZero.iUnion (ι := T) this
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))
U : M → Set M := fun x => (ChartedSpace.chartAt x).source
⊢ univ ⊆ ⋃ x, U x
Tactic:
intro 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
x : M
a✝ : x ∈ univ
⊢ x ∈ ⋃ x, U x
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
x : M
a✝ : x ∈ univ
⊢ x ∈ ⋃ x, U x
Tactic:
rw [mem_iUnion]
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
x : M
a✝ : x ∈ univ
⊢ ∃ i, x ∈ U i
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
x : M
a✝ : x ∈ univ
⊢ ∃ i, x ∈ U i
Tactic:
exact ⟨x, mem_chart_source H x⟩
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))
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
⊢ ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
intro i
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
i : ↑T
⊢ MeasureZero J (f '' (U ↑i ∩ 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
i : ↑T
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
let e : PartialHomeomorph M H := ChartedSpace.chartAt i
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
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
⊢ MeasureZero J (f '' (U ↑i ∩ 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
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
have h : MeasureZero J (f '' (e.source ∩ s)) := hs i
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
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ MeasureZero J (f '' (U ↑i ∩ 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
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ MeasureZero J (f '' (U ↑i ∩ s))
Tactic:
have h₃ : U i = e.source := by rw [← Filter.principal_eq_iff_eq]
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
i : ↑T
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
h₃ : U ↑i = e.source
⊢ MeasureZero J (f '' (U ↑i ∩ s))