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
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))
Tactic:
apply h.mono _
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
⊢ f '' (U ↑i ∩ s) ⊆ f '' (e.source ∩ 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))
h₃ : U ↑i = e.source
⊢ f '' (U ↑i ∩ s) ⊆ f '' (e.source ∩ s)
Tactic:
apply image_subset
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✝²⁰ : 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
⊢ U ↑i ∩ s ⊆ e.source ∩ s
Theorem: measure_zero_image_iff_chart_domains
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✝²⁰ : 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
⊢ U ↑i ∩ s ⊆ e.source ∩ s
Tactic:
rw [h₃]
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
e : PartialHomeomorph M H := ChartedSpace.chartAt ↑i
h : MeasureZero J (f '' (e.source ∩ s))
⊢ U ↑i = e.source
Tactic:
rw [← Filter.principal_eq_iff_eq]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ ⋃ i, f '' (U ↑i ∩ s) = f '' ⋃ i, U ↑i ∩ s
Tactic:
rw [image_iUnion]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ⋃ i, U ↑i ∩ s = f '' ((⋃ i, U ↑i) ∩ s)
Tactic:
rw [iUnion_inter]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i, U ↑i) ∩ s) = f '' ((⋃ i ∈ T, U i) ∩ s)
Tactic:
rw [iUnion_coe_set]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i ∈ T, U i) ∩ s) = f '' ((⋃ i, U i) ∩ s)
Tactic:
rw [hTcover]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' ((⋃ i, U i) ∩ s) = f '' (univ ∩ s)
Tactic:
rw [subset_antisymm (by simp) (hcovering)]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ ⋃ x, U x ⊆ univ
Tactic:
simp
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
⊢ f '' (univ ∩ s) = f '' s
Tactic:
rw [univ_inter]
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
this : ∀ (i : ↑T), MeasureZero J (f '' (U ↑i ∩ s))
decomp : ⋃ i, f '' (U ↑i ∩ s) = f '' s
⊢ Encodable ↑T
Tactic:
sorry
Proof state after:
no goals
Theorem: MeasureZero.isMeagre_of_isSigmaCompact
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
inst✝ : T2Space N
s : Set N
h₁s : MeasureZero J s
h₂s : IsSigmaCompact s
⊢ IsMeagre s
Tactic:
obtain ⟨K, ⟨hcompact, hcover⟩⟩ := h₂s
Proof state after:
case intro.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✝²¹ : 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
inst✝ : T2Space N
s : Set N
h₁s : MeasureZero J s
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
⊢ IsMeagre s