α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
⊢ WeaklyRegular (restrict μ A)
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
⊢ WeaklyRegular (restrict μ A)
haveI : Fact (μ A < ∞) := ⟨h'A.lt_top⟩
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
⊢ ∀ (r : ℝ≥0∞), r < ↑↑(restrict μ A) V → ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑(restrict μ A) K
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
⊢ WeaklyRegular (restrict μ A)
refine' InnerRegular.weaklyRegular_of_finite (μ.restrict A) fun V V_open => _
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
⊢ ∀ (r : ℝ≥0∞), r < ↑↑μ (V ∩ A) → ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
⊢ ∀ (r : ℝ≥0∞), r < ↑↑(restrict μ A) V → ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑(restrict μ A) K
simp only [restrict_apply' hA]
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
⊢ ∀ (r : ℝ≥0∞), r < ↑↑μ (V ∩ A) → ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
intro r hr
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
have : μ (V ∩ A) ≠ ∞ := ne_top_of_le_ne_top h'A (measure_mono <| inter_subset_right _ _)
case intro.intro.intro
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
F : Set α
hFVA : F ⊆ V ∩ A
hFc : IsClosed F
hF : r < ↑↑μ F
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
rcases(V_open.measurableSet.inter hA).exists_lt_isClosed_of_ne_top this hr with
  ⟨F, hFVA, hFc, hF⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
F : Set α
hFVA : F ⊆ V ∩ A
hFc : IsClosed F
hF : r < ↑↑μ F
⊢ r < ↑↑μ (F ∩ A)
case intro.intro.intro
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
F : Set α
hFVA : F ⊆ V ∩ A
hFc : IsClosed F
hF : r < ↑↑μ F
⊢ ∃ K, K ⊆ V ∧ IsClosed K ∧ r < ↑↑μ (K ∩ A)
refine' ⟨F, hFVA.trans (inter_subset_left _ _), hFc, _⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.77698
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : BorelSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
this✝ : Fact (↑↑μ A < ⊤)
V : Set α
V_open : IsOpen V
r : ℝ≥0∞
hr : r < ↑↑μ (V ∩ A)
this : ↑↑μ (V ∩ A) ≠ ⊤
F : Set α
hFVA : F ⊆ V ∩ A
hFc : IsClosed F
hF : r < ↑↑μ F
⊢ r < ↑↑μ (F ∩ A)
rwa [inter_eq_self_of_subset_left (hFVA.trans <| inter_subset_right _ _)]