diamonds

Stream: maths

[Sebastien Gouezel]

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...

[Patrick Massot]

Isn't this rfl?

[Mario Carneiro]

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

[Mario Carneiro]

it all depends on the implicits though

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Sebastien Gouezel]

PRed in #1551