# Zulip Chat Archive

## Stream: new members

### Topic: Products induces topology on fibers

#### Nicolò Cavalleri (Dec 20 2020 at 10:58):

I got a bit rusty: how do I prove something like this (supposing it says what I want to say)

```
example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
∀ x : X, inducing (λ y : Y, prod.mk x y) := sorry
```

?

#### Mario Carneiro (Dec 20 2020 at 11:24):

One direction is going to be continuity of `prod.mk`

#### Mario Carneiro (Dec 20 2020 at 11:33):

```
example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y]
(x : X) : inducing (λ y : Y, prod.mk x y) :=
begin
refine ⟨le_antisymm (continuous_const.prod_mk continuous_id).le_induced (λ s h, _)⟩,
convert is_open_induced (is_open_univ.prod h),
ext x, simp
end
```

#### Nicolò Cavalleri (Dec 20 2020 at 11:51):

Ok thanks! I was trying this way:

```
lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
t.induced (λ y : Y, x) = ⊤ := by { sorry, }
example {X : Type*} {Y : Type*} [topological_space X] [topological_space Y] :
∀ x : X, inducing (λ y : Y, prod.mk x y) := λ z,
⟨by {rw prod.topological_space,
simp only [induced_inf, induced_compose, function.comp, constant_induces_top, top_inf_eq],
rw [induced_id], }⟩
```

but the last rw does not work... do you know why? (I missed a bit when I first pasted it, sorry)

#### Nicolò Cavalleri (Dec 20 2020 at 12:37):

Also what is a smart way to prove

```
lemma constant_induces_top {X : Type*} {Y : Type*} [t : topological_space X] {x : X} :
t.induced (λ y : Y, x) = ⊤ := sorry
```

without going back to definitions?

#### Reid Barton (Dec 20 2020 at 12:40):

It's equivalent to the statement with `>=`

, which is equivalent to `λ y : Y, x`

being continuous w.r.t. `⊤`

(or any topology), which is `continuous_const`

#### Nicolò Cavalleri (Dec 20 2020 at 13:04):

Ok thanks. Is the name `constant_induces_top`

appropriate?

#### Nicolò Cavalleri (Dec 20 2020 at 13:06):

Also my proof above works if I add this lemma

```
lemma induced_id' {α : Type*} [t : topological_space α] : t.induced (λ a : α, a) = t := induced_id
```

What should I do? Should this new lemma go into mathlib or should I report that `id`

is not working properly?

#### Reid Barton (Dec 20 2020 at 13:11):

`id`

isn't reducible so there is no surprise here

#### Reid Barton (Dec 20 2020 at 13:13):

Nicolò Cavalleri said:

Ok thanks. Is the name

`constant_induces_top`

appropriate?

I think we would call it something more like `induced_const`

#### Nicolò Cavalleri (Dec 20 2020 at 13:13):

Ok should we change the statement of `induced_id`

? Or what solution do you propose?

#### Reid Barton (Dec 20 2020 at 13:15):

I don't really think any action is needed

#### Reid Barton (Dec 20 2020 at 13:15):

You could finish with `exact induced_id.symm`

#### Reid Barton (Dec 20 2020 at 13:16):

Certainly adding a lemma would be better than changing an existing lemma, but I'm not sure if it will ever see real use

#### Reid Barton (Dec 20 2020 at 13:19):

I'm not really sure if there is a reason that `function.comp`

is reducible but not `id`

... it is a bit confusing

Last updated: May 17 2021 at 22:15 UTC