Theorem: MeasureZero.isMeagre_of_isSigmaCompact (Sard/MeasureZero.lean)

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
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

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⟩
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)

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
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)

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)
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)

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))
State after:
no goals

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]
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

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]
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

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⟩
State after:
no goals