internlm/Lean-Github huggingface dataset:
Theorem: MeasureZero.isMeagre_of_isSigmaCompact
Proof state before:
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
Tactic:
suffices ∀ n : ℕ, IsNowhereDense (K n) by
  rw [isMeagre_iff_countable_union_isNowhereDense, ← hcover]
  simp [IsMeagre]
  exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ this n, countable_range K, fun i ↦ subset_iUnion K i⟩
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
⊢ ∀ (n : ℕ), IsNowhereDense (K n)
Theorem: MeasureZero.isMeagre_of_isSigmaCompact
Proof state before:
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
⊢ ∀ (n : ℕ), IsNowhereDense (K n)
Tactic:
intro n
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
n : ℕ
⊢ IsNowhereDense (K n)
Theorem: MeasureZero.isMeagre_of_isSigmaCompact
Proof state before:
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
n : ℕ
⊢ IsNowhereDense (K n)
Tactic:
have h : MeasureZero J (K n) := h₁s.mono (hcover ▸ subset_iUnion K n)
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
n : ℕ
h : MeasureZero J (K n)
⊢ IsNowhereDense (K n)
Theorem: MeasureZero.isMeagre_of_isSigmaCompact
Proof state before:
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
n : ℕ
h : MeasureZero J (K n)
⊢ IsNowhereDense (K n)
Tactic:
exact MeasureZero.isNowhereDense_of_isClosed J h (IsCompact.isClosed (hcompact n))
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
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
this : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ IsMeagre s
Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense, ← hcover]
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
inst✝ : T2Space N
s : Set N
h₁s : MeasureZero J s
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
this : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ ⋃ n, K n ⊆ S.sUnion
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
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
this : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ ⋃ n, K n ⊆ S.sUnion
Tactic:
simp [IsMeagre]
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
inst✝ : T2Space N
s : Set N
h₁s : MeasureZero J s
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
this : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ ∀ (i : ℕ), K i ⊆ S.sUnion
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
K : ℕ → Set N
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
this : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ ∀ (i : ℕ), K i ⊆ S.sUnion
Tactic:
exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ this n, countable_range K, fun i ↦ subset_iUnion K i⟩
Proof state after:
no goals
Theorem: PartialHomeomorph.isOpenMapOn_source
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (↑e '' s)
Tactic:
rw [(image_eq_target_inter_inv_preimage (e := e) hs)]
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
Theorem: PartialHomeomorph.isOpenMapOn_source
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
Tactic:
exact e.continuousOn_invFun.isOpen_inter_preimage e.open_target hopen
Proof state after:
no goals
Theorem: PartialHomeomorph.symm_isOpenMapOn_target
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
⊢ IsOpen (e.invFun '' t)
Tactic:
have r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t := symm_image_eq_source_inter_preimage (e := e) ht
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t
⊢ IsOpen (e.invFun '' t)
Theorem: PartialHomeomorph.symm_isOpenMapOn_target
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✝ : SmoothManifoldWithCorners I M
e : PartialHomeomorph M H
t : Set H
hopen : IsOpen t
ht : t ⊆ e.target
r : e.invFun '' t = e.source ∩ ↑e ⁻¹' t
⊢ IsOpen (e.invFun '' t)
Tactic:
exact r ▸ e.continuousOn_toFun.isOpen_inter_preimage e.open_source hopen
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_isOpenMapOn_source
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (↑(e.extend I) '' s)
Tactic:
simp only [extend_coe, image_comp I e]
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (↑I '' (↑e '' s))
Theorem: PartialHomeomorph.extend_isOpenMapOn_source
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
s : Set M
hopen : IsOpen s
hs : s ⊆ e.source
⊢ IsOpen (↑I '' (↑e '' s))
Tactic:
apply (I.toOpenEmbedding.open_iff_image_open).mp (e.isOpenMapOn_source hopen hs)
Proof state after:
no goals
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have h : IsOpen (I.invFun '' t) := I.toOpenEmbedding_symm.open_iff_image_open.mp 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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
⊢ IsOpen (↑(e.extend I).symm '' t)
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have : (e.extend I).target = I.symm ⁻¹' e.target := by
  let r := e.extend_target I
  rw [I.range_eq_univ, inter_univ] at r
  exact r
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this : (e.extend I).target = ↑I.symm ⁻¹' e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
have : I.symm '' t ⊆ e.target := calc I.symm '' t
  _ ⊆ I.symm '' ((e.extend I).target) := image_subset _ ht
  _ = I.symm '' (I.symm ⁻¹' e.target) := by rw [this]
  _ ⊆ e.target := image_preimage_subset I.symm e.target
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Theorem: PartialHomeomorph.extend_symm_isOpenMapOn_target
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑(e.extend I).symm '' t)
Tactic:
rw [extend_coe_symm, 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✝¹ : SmoothManifoldWithCorners I M
inst✝ : I.Boundaryless
e : PartialHomeomorph M H
t : Set E
hopen : IsOpen t
ht : t ⊆ (e.extend I).target
h : IsOpen (I.invFun '' t)
this✝ : (e.extend I).target = ↑I.symm ⁻¹' e.target
this : ↑I.symm '' t ⊆ e.target
⊢ IsOpen (↑e.symm '' (↑I.symm '' t))