## Stream: maths

### Topic: continuous function to pi type

#### Johan Commelin (May 23 2018 at 09:58):

I have no clue how to prove this:

lemma continuous.pi_mk {X I : Type*} {Y : I → Type*}
[topological_space X] [Πi, topological_space (Y i)] (f : Πi, X → (Y i)) (H : Πi, continuous (f i))
: continuous (λ x i, f i x) := sorry


#### Kevin Buzzard (May 23 2018 at 09:59):

Can you prove it in maths?

:-)

#### Kevin Buzzard (May 23 2018 at 09:59):

i.e. "is it true"

#### Johan Commelin (May 23 2018 at 09:59):

Unless I made a stupid mistake: yes

#### Mario Carneiro (May 23 2018 at 10:00):

how is the pi topology defined?

#### Johan Commelin (May 23 2018 at 10:00):

It just says that Pi is some sort of categorical product on steroids

what Mario said

#### Johan Commelin (May 23 2018 at 10:00):

If I have continuous maps to all the factors, I get a continuous map to the Pi

(in Lean)

#### Johan Commelin (May 23 2018 at 10:00):

instance Pi.topological_space {β : α → Type v} [t₂ : Πa, topological_space (β a)]
: topological_space (Πa, β a) :=
⨆a, topological_space.induced (λf, f a) (t₂ a)


#### Mario Carneiro (May 23 2018 at 10:01):

so look for theorems about continuity on induced

#### Johan Commelin (May 23 2018 at 10:01):

There are loads of those... but how do I deal with the ⨆a, that is in front?

#### Mario Carneiro (May 23 2018 at 10:01):

look for continuity on a Sup

#### Johan Commelin (May 23 2018 at 10:02):

there is only continuity for sup, not Sup

#### Mario Carneiro (May 23 2018 at 10:03):

I think it's called that... serach for the bigcup

#### Johan Commelin (May 23 2018 at 10:03):

I'm already down 5 rabbit holes, I really hope I don't need to go down this one as well...

#### Johan Commelin (May 23 2018 at 10:03):

Search for ⨆ gives No results in continuity.lean

#### Mario Carneiro (May 23 2018 at 10:04):

hm, looks like it is missing from the list at continuity.lean

#### Johan Commelin (May 23 2018 at 10:05):

Right, there is constructors for products of two topological spaces, and continous maps towards them, etc... but for Pi types this seems missing. And I don't know exactly how to prove this stuff...

#### Johan Commelin (May 23 2018 at 10:06):

/me doesn't know anything about Sup and friends

#### Mario Carneiro (May 23 2018 at 10:06):

okay, so use the existing theorems as guides and write your own version for continuity on supr

#### Johan Commelin (May 23 2018 at 10:06):

\me goes down rabbit hole # 6

#### Mario Carneiro (May 23 2018 at 10:06):

(or I can, if this is going too far afield)

#### Mario Carneiro (May 23 2018 at 10:06):

I'm just showing you what I would do

#### Johan Commelin (May 23 2018 at 10:07):

Well, I'm trying to prove that the face map between two standard simplices is continuous...

#### Johan Commelin (May 23 2018 at 10:08):

@Mario Carneiro At the moment, I don't even know how to write the statement for Sup

#### Mario Carneiro (May 23 2018 at 10:20):

here you go:

lemma continuous_Sup_dom {t₁ : set (tspace α)} {t₂ : tspace β}
{t : tspace α} (h₁ : t ∈ t₁) : cont t t₂ f → cont (Sup t₁) t₂ f :=
continuous_le_dom (le_Sup h₁)

lemma continuous_Sup_rng {t₁ : tspace α} {t₂ : set (tspace β)}
(h : ∀t∈t₂, cont t₁ t f) : cont t₁ (Sup t₂) f :=
continuous_Inf_rng
(λ t ht, show t ≤ coinduced f t₁, from h t ht)
continuous_coinduced_rng

lemma continuous_supr_dom {t₁ : ι → tspace α} {t₂ : tspace β}
{i : ι} : cont (t₁ i) t₂ f → cont (supr t₁) t₂ f :=
continuous_Sup_dom ⟨i, rfl⟩

lemma continuous_supr_rng {t₁ : tspace α} {t₂ : ι → tspace β}
(h : ∀i, cont t₁ (t₂ i) f) : cont t₁ (supr t₂) f :=


#### Johannes Hölzl (May 23 2018 at 12:49):

For the sum proof: its easiest to generalize for finset, and then go from list to multiset to finset. I will add this to mathlib:

lemma continuous_supr_rng
{ι : Sort*} {α : Type*} {β : Type*} {t₁ : topological_space α} {t₂ : ι → topological_space β}
{f : α → β}
(h : ∀i, @continuous _ _ t₁ (t₂ i) f) :
@continuous _ _ t₁ (lattice.supr t₂) f :=
continuous_iff_le_coinduced.2 $lattice.supr_le$ assume i, continuous_iff_le_coinduced.1 (h i)

lemma continuous.pi_mk
{X I : Type*} {Y : I → Type*} [t₁ : topological_space X] [t₂ : Πi, topological_space (Y i)]
(f : Πi, X → (Y i)) (H : Πi, continuous (f i)) :
continuous (λ x i, f i x) :=
continuous_supr_rng $assume i, continuous_induced_rng$ H i

lemma continuous_list_sum {α : Type*} {β : Type*} {γ : Type*}
{f : γ → α → β} :
∀l:list γ, (∀c∈l, continuous (f c)) → continuous (λa, (l.map (λc, f c a)).sum)
| []       _ := by simp [continuous_const]
| (f :: l) h :=
begin
simp,
(h f (list.mem_cons_self _ _))
(continuous_list_sum l (assume c hc, h c (list.mem_cons_of_mem _ hc)))
end

lemma continuous_multiset_sum {α : Type*} {β : Type*} {γ : Type*}
{f : γ → α → β} (s : multiset γ) :
(∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).sum) :=


#### Patrick Massot (May 23 2018 at 15:06):

Hum, I think I stupidly missed the eq.symm when I tried

#### Johannes Hölzl (May 23 2018 at 15:31):

@Johan Commelin I forgot that there is already tendsto_sum, so you could also derive continuous_finset_sum from this.
Anyway, this all is now in mathlib.

#### Johan Commelin (May 23 2018 at 16:54):

Thanks a lot! I will merge into my fork. Once I clean my stuff up, I think I will make a PR

Last updated: May 18 2021 at 08:14 UTC