α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ↑m t ≤ 0
⊢ ↑m s = 0
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ↑m s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∀ (t : Set α), t ∈ 𝓝[s] x → 0 < ↑m t
contrapose! hs
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
⊢ ↑m s = 0
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ↑m t ≤ 0
⊢ ↑m s = 0
simp only [nonpos_iff_eq_zero, ← exists_prop] at hs
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
⊢ ∀ (x : α), x ∈ s → ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
⊢ ↑m s = 0
apply m.null_of_locally_null s
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
x : α
hx : x ∈ s
⊢ ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
⊢ ∀ (x : α), x ∈ s → ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
intro x hx
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
x : α
hx : x ∈ s
hs : ∃ t _h, ↑m t = 0
⊢ ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
hs : ∀ (x : α), x ∈ s → ∃ t _h, ↑m t = 0
x : α
hx : x ∈ s
⊢ ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
specialize hs x hx
no goals
α : Type u_1
β : Type ?u.10003
R : Type ?u.10006
R' : Type ?u.10009
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
inst✝¹ : TopologicalSpace α
inst✝ : SecondCountableTopology α
m : OuterMeasure α
s : Set α
x : α
hx : x ∈ s
hs : ∃ t _h, ↑m t = 0
⊢ ∃ u, u ∈ 𝓝[s] x ∧ ↑m u = 0
exact Iff.mp bex_def hs