Zulip Chat Archive

Stream: maths

Topic: diamonds


view this post on Zulip Sebastien Gouezel (Oct 14 2019 at 14:11):

I thought our topology library was written with enough care to take care of diamonds, but apparently this is not the case:

lemma diamond {n : } : is_open (pi (univ : set (fin n)) (λi, (univ : set ))) :=
begin
  have A : finite (univ : set (fin n)) := finite_univ,
  have B : i : fin n, i  univ  is_open (univ : set ) := λi hi, is_open_univ,
  convert is_open_set_pi A B,
end

leaves me with the goal uniform_space.to_topological_space (fin n → ℝ) = Pi.topological_space. I know how to fix this, but it is always suprising to find these...

view this post on Zulip Patrick Massot (Oct 14 2019 at 14:12):

Isn't this rfl?

view this post on Zulip Mario Carneiro (Oct 14 2019 at 14:14):

I don't see how that could be anything other than rfl

view this post on Zulip Mario Carneiro (Oct 14 2019 at 14:14):

it all depends on the implicits though

view this post on Zulip Sebastien Gouezel (Oct 14 2019 at 14:31):

No, it's not refl, because some definition has not set up carefully enough the uniform space structure and the topological space structure on the product. Maybe it comes from

instance fintype.normed_group {π : ι  Type*} [fintype ι] [i, normed_group (π i)] :
  normed_group (Πb, π b) :=
{ norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : nnreal) : ),
  dist_eq := assume x y,
    congr_arg (coe : nnreal  ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
    show nndist (x a) (y a) = nnnorm (x a - y a), from nndist_eq_nnnorm _ _ }

I'll fix this.

view this post on Zulip Johan Commelin (Oct 14 2019 at 14:34):

Also, that names seems bad. Shouldn't that be pi.normed_group?

view this post on Zulip Sebastien Gouezel (Oct 14 2019 at 21:29):

PRed in #1551


Last updated: May 12 2021 at 08:14 UTC