ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h
rw [iInf_mul]
no goals
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h
exact le_ciInf H