α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ a ∈ v ∧ v ⊆ u
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ ↑↑μ s < ⊤}
refine' TopologicalSpace.isTopologicalBasis_of_open_of_nhds (fun s hs => hs.1) _
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
⊢ ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ x ∈ v ∧ v ⊆ s
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ a ∈ v ∧ v ⊆ u
intro x s xs hs
case intro.intro.intro
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : ↑↑μ v < ⊤
⊢ ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ x ∈ v ∧ v ⊆ s
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
⊢ ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ x ∈ v ∧ v ⊆ s
rcases μ.exists_isOpen_measure_lt_top x with ⟨v, xv, hv, μv⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : ↑↑μ v < ⊤
⊢ ↑↑μ (v ∩ s) ≤ ↑↑μ v
case intro.intro.intro
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : ↑↑μ v < ⊤
⊢ ∃ v, v ∈ {s | IsOpen s ∧ ↑↑μ s < ⊤} ∧ x ∈ v ∧ v ⊆ s
refine' ⟨v ∩ s, ⟨hv.inter hs, lt_of_le_of_lt _ μv⟩, ⟨xv, xs⟩, inter_subset_right _ _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.831042
γ : Type ?u.831045
δ : Type ?u.831048
ι : Type ?u.831051
R : Type ?u.831054
R' : Type ?u.831057
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
x : α
s : Set α
xs : x ∈ s
hs : IsOpen s
v : Set α
xv : x ∈ v
hv : IsOpen v
μv : ↑↑μ v < ⊤
⊢ ↑↑μ (v ∩ s) ≤ ↑↑μ v
exact measure_mono (inter_subset_left _ _)