ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) ↔
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ n ≤ OuterMeasure.pi m ↔
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
rw [OuterMeasure.pi, le_boundedBy']
case mp
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)

case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) ↔
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
constructor
case mp
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
s : (i : ι) → Set (α i)
hs : Set.Nonempty (Set.pi univ s)
⊢ ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
case mp
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
intro h s hs
no goals
case mp
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
s : (i : ι) → Set (α i)
hs : Set.Nonempty (Set.pi univ s)
⊢ ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
refine' (h _ hs).trans_eq (piPremeasure_pi hs)
case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ ↑n s ≤ piPremeasure m s
case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), Set.Nonempty s → ↑n s ≤ piPremeasure m s
intro h s hs
case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ Set.Nonempty (Set.pi univ fun i => eval i '' s)
case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ ↑n s ≤ piPremeasure m s
refine' le_trans (n.mono <| subset_pi_eval_image univ s) (h _ _)
no goals
case mpr
ι : Type u_2
ι' : Type ?u.2059615
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), Set.Nonempty (Set.pi univ s) → ↑n (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
s : Set ((i : ι) → α i)
hs : Set.Nonempty s
⊢ Set.Nonempty (Set.pi univ fun i => eval i '' s)
simp [univ_pi_nonempty_iff, hs]