## Stream: maths

### Topic: diamonds

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

#### Patrick Massot (Oct 14 2019 at 14:12):

Isn't this rfl?

#### Mario Carneiro (Oct 14 2019 at 14:14):

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

#### Mario Carneiro (Oct 14 2019 at 14:14):

it all depends on the implicits though

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

#### Johan Commelin (Oct 14 2019 at 14:34):

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

#### Sebastien Gouezel (Oct 14 2019 at 21:29):

PRed in #1551

Last updated: May 12 2021 at 08:14 UTC