α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ↑(↑(comap f) (⨅ (i : ι), m i)) s = ↑(⨅ (i : ι), ↑(comap f) (m i)) s
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
⊢ ↑(comap f) (⨅ (i : ι), m i) = ⨅ (i : ι), ↑(comap f) (m i)
refine' ext_nonempty fun s hs => _
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ↑(⨅ (i : ι), ↑(comap f) (m i)) s ≤ ↑(↑(comap f) (⨅ (i : ι), m i)) s
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ↑(↑(comap f) (⨅ (i : ι), m i)) s = ↑(⨅ (i : ι), ↑(comap f) (m i)) s
refine' ((comap_mono f).map_iInf_le s).antisymm _
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ∀ (i : ℕ → Set β),
    (s ⊆ ⋃ (i_1 : ℕ), f ⁻¹' i i_1) →
      (⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' t n)) ≤
        ∑' (n : ℕ), ⨅ (i_2 : ι), ↑(m i_2) (i n)
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ↑(⨅ (i : ι), ↑(comap f) (m i)) s ≤ ↑(↑(comap f) (⨅ (i : ι), m i)) s
simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff,
  Set.image_subset_iff, preimage_iUnion]
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
t : ℕ → Set β
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
k : ℕ
⊢ (⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' t k))) ≤ ⨅ (i : ι), ↑(m i) (t k)
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
⊢ ∀ (i : ℕ → Set β),
    (s ⊆ ⋃ (i_1 : ℕ), f ⁻¹' i i_1) →
      (⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' t n)) ≤
        ∑' (n : ℕ), ⨅ (i_2 : ι), ↑(m i_2) (i n)
refine' fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => _)
no goals
α : Type u_3
ι : Sort u_1
β : Type u_2
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : Set.Nonempty s
t : ℕ → Set β
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
k : ℕ
⊢ (⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' t k))) ≤ ⨅ (i : ι), ↑(m i) (t k)
exact iInf_mono fun i => (m i).mono (image_preimage_subset _ _)