α : Type u_1
β : Type ?u.9276
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
⊢ (⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U) ≤ ↑↑μ A
α : Type u_1
β : Type ?u.9276
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
⊢ ↑↑μ A = ⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U
refine' le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) _
α : Type u_1
β : Type ?u.9276
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
r : ℝ≥0∞
hr : ↑↑μ A < r
⊢ (⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U) < r
α : Type u_1
β : Type ?u.9276
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
⊢ (⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U) ≤ ↑↑μ A
refine' le_of_forall_lt' fun r hr => _
no goals
α : Type u_1
β : Type ?u.9276
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
r : ℝ≥0∞
hr : ↑↑μ A < r
⊢ (⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), ↑↑μ U) < r
simpa only [iInf_lt_iff, exists_prop] using A.exists_isOpen_lt_of_lt r hr