α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
s : Set β
⊢ ↑(OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
s : Set β
⊢ ↑(↑(map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)
rw [map_apply]
no goals
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
s : Set β
⊢ ↑(OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)
apply ofFunction_le