Zulip Chat Archive

Stream: Is there code for X?

Topic: Inf of scalar product


view this post on Zulip Bhavik Mehta (Apr 13 2021 at 19:33):

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?

view this post on Zulip Yury G. Kudryashov (Apr 13 2021 at 20:09):

We have docs#map_cInf_of_continuous_at_of_monotone

view this post on Zulip Bhavik Mehta (Apr 13 2021 at 22:50):

Thanks Yury!

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

does what I wanted


Last updated: May 07 2021 at 22:14 UTC