α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
⊢ ↑m s = 0
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
⊢ ↑m s = 0
choose! u hxu hu₀ using hs
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ht : t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m s = 0
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
⊢ ↑m s = 0
choose t ht using TopologicalSpace.countable_cover_nhdsWithin hxu
case intro.intro
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ts : t ⊆ s
t_count : Set.Countable t
ht : s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m s = 0
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ht : t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m s = 0
rcases ht with ⟨ts, t_count, ht⟩
case intro.intro
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ts : t ⊆ s
t_count : Set.Countable t
ht : s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m (⋃ (x : α) (_ : x ∈ t), u x) = 0
case intro.intro
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ts : t ⊆ s
t_count : Set.Countable t
ht : s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m s = 0
apply m.mono_null ht
no goals
case intro.intro
α : Type u_1
β : Type ?u.9450
R : Type ?u.9453
R' : Type ?u.9456
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
u : α → Set α
hxu : ∀ (x : α), x ∈ s → u x ∈ 𝓝[s] x
hu₀ : ∀ (x : α), x ∈ s → ↑m (u x) = 0
t : Set α
ts : t ⊆ s
t_count : Set.Countable t
ht : s ⊆ ⋃ (x : α) (_ : x ∈ t), u x
⊢ ↑m (⋃ (x : α) (_ : x ∈ t), u x) = 0
exact (m.biUnion_null_iff t_count).2 fun x hx => hu₀ x (ts hx)