α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ ↑(map f) (⨅ (i : ι), m i) = ↑(map f) (↑(comap f) (⨅ (i : ι), ↑(map f) (m i)))
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ ↑(map f) (⨅ (i : ι), m i) = ↑(restrict (range f)) (⨅ (i : ι), ↑(map f) (m i))
refine' Eq.trans _ (map_comap _ _)
no goals
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ ↑(map f) (⨅ (i : ι), m i) = ↑(map f) (↑(comap f) (⨅ (i : ι), ↑(map f) (m i)))
simp only [comap_iInf, comap_map hf]