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