α : Type u_3
ι : Type u_1
β : Type u_2
I : Set ι
hI : Set.Nonempty I
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ ↑(map f) (⨅ (i : ι) (_ : i ∈ I), ↑(comap f) (m i)) = ⨅ (i : ι) (_ : i ∈ I), ↑(map f) (↑(comap f) (m i))
α : Type u_3
ι : Type u_1
β : Type u_2
I : Set ι
hI : Set.Nonempty I
f : α → β
m : ι → OuterMeasure β
⊢ ↑(map f) (⨅ (i : ι) (_ : i ∈ I), ↑(comap f) (m i)) = ⨅ (i : ι) (_ : i ∈ I), ↑(map f) (↑(comap f) (m i))
haveI := hI.to_subtype
α : Type u_3
ι : Type u_1
β : Type u_2
I : Set ι
hI : Set.Nonempty I
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ ↑(map f) (⨅ (i : ↑I), ↑(comap f) (m ↑i)) = ⨅ (i : ↑I), ↑(map f) (↑(comap f) (m ↑i))
α : Type u_3
ι : Type u_1
β : Type u_2
I : Set ι
hI : Set.Nonempty I
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ ↑(map f) (⨅ (i : ι) (_ : i ∈ I), ↑(comap f) (m i)) = ⨅ (i : ι) (_ : i ∈ I), ↑(map f) (↑(comap f) (m i))
rw [← iInf_subtype'', ← iInf_subtype'']
no goals
α : Type u_3
ι : Type u_1
β : Type u_2
I : Set ι
hI : Set.Nonempty I
f : α → β
m : ι → OuterMeasure β
this : Nonempty ↑I
⊢ ↑(map f) (⨅ (i : ↑I), ↑(comap f) (m ↑i)) = ⨅ (i : ↑I), ↑(map f) (↑(comap f) (m ↑i))
exact map_iInf_comap _