case inl
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.pi univ s = ∅
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)

case inr
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
cases' (pi univ s).eq_empty_or_nonempty with h h
case inr
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
case inl
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.pi univ s = ∅
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)

case inr
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
simp [h]
no goals
case inr
ι : Type u_2
ι' : Type ?u.1844425
α : ι → Type u_1
inst✝ : Fintype ι
m✝ m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.Nonempty (Set.pi univ s)
⊢ ↑(OuterMeasure.pi m) (Set.pi univ s) ≤ ∏ i : ι, ↑(m i) (s i)
exact (boundedBy_le _).trans_eq (piPremeasure_pi h)