Inf of scalar product

Stream: Is there code for X?

[Bhavik Mehta]

import data.real.basic

example (K : set ℝ) (hK₁ : K.nonempty) (hK₂ : bdd_below K) : Inf (2 • K) = 2 * Inf K :=
begin
  library_search
end

or anything to this effect?

[Yury G. Kudryashov]

We have docs#map_cInf_of_continuous_at_of_monotone

[Bhavik Mehta]

Thanks Yury!

example (K : set ℝ) (θ : ℝ) (hθ : 0 ≤ θ) (hK : K.nonempty) (bd : bdd_below K) :
  Inf (θ • K) = θ * Inf K :=
begin
  have : monotone (λ x, (θ:ℝ) * x),
  { exact monotone_mul_left_of_nonneg hθ },
  have z := map_cInf_of_continuous_at_of_monotone (continuous_mul_left θ).continuous_at
                (monotone_mul_left_of_nonneg hθ) hK bd,
  dsimp at z,
  rw [z, ←set.image_smul],
  refl,
end

does what I wanted