{lo hi : ℕ → ℝ} {lam mu : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) {m : ℕ} (hlo : mu ≤ lo m) : mu ≤ lam

Initializing...

{lo hi : ℕ → ℝ} {lam mu : ℝ} (hmem : ∀ m, lam ∈ Set.Icc (lo m) (hi m)) {m : ℕ} (hlo : mu ≤ lo m) : mu ≤ lam · Prove2Me