# Zulip Chat Archive

## 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):

:-)

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

#### Kevin Buzzard (May 23 2018 at 10:00):

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

#### Kevin Buzzard (May 23 2018 at 10:00):

(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 := continuous_Sup_rng $ assume t ⟨i, (t_eq : t = t₂ i)⟩, t_eq.symm ▸ h i

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

I just copied the Inf stuff and dualized everything

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

Ok, thanks!

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

Let me see if I can continue with rabbit hole # 5 (-;

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

Hurray!

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) := begin let YY := (Πi, Y i), apply continuous_Sup_rng, intros t ht, cases ht with i hi, simp at *, rw hi, apply continuous_induced_rng, unfold function.comp, exact H i, end

#### Johan Commelin (May 23 2018 at 11:23):

Ok, so now I'm stuck with this MWE:

lemma continuous_sums {n : ℕ} : continuous (λ x : ((fin n) → ℝ), univ.sum x) := sorry

#### Johan Commelin (May 23 2018 at 11:24):

Whatever I try, I'm pulled hard into all sorts of `foldr`

stuff. And I'm completely out of my comfort zone.

#### Mario Carneiro (May 23 2018 at 11:24):

that's not a trivial theorem

#### Johan Commelin (May 23 2018 at 11:25):

I would like to mumble some think like... well, addition is continuous... if you repeatedly add, you get continuity by induction

#### Johan Commelin (May 23 2018 at 11:25):

Can I `foldr`

the continuity proof off `add`

?

#### Mario Carneiro (May 23 2018 at 11:25):

I guess you can prove it by induction on `n`

, you will need to show that `fin (succ n) -> R`

is homeomorphic to `R x (fin n -> R)`

#### Johan Commelin (May 23 2018 at 11:27):

To link back to the discussion with Kevin, from about an hour ago... do you think this could be made into a trivial theorem?

#### Mario Carneiro (May 23 2018 at 11:27):

no

#### Mario Carneiro (May 23 2018 at 11:28):

okay, maybe that's too strong, you might be able to prove it by induction on the set instead

#### Johan Commelin (May 23 2018 at 11:29):

that sounds closer to what I wanted to mumble

#### Mario Carneiro (May 23 2018 at 11:29):

in that case you want to use `finset.induction_on`

#### Mario Carneiro (May 23 2018 at 11:30):

and the IH says that a sum of continuous functions over set s is continuous

#### Johan Commelin (May 23 2018 at 11:33):

Ok, I'm going to try this. Thanks!

#### Patrick Massot (May 23 2018 at 12:43):

Johan, you may already know, but just in case: there very easy clean up steps you can run on such proofs. `YY`

is never used. `unfold`

is actually much less useful that one thinks in the beginning, so I always try to remove all `unfold`

once a proof work. And then we always try to get rid of `simp`

in the middle of proofs. The result is:

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) := begin apply continuous_Sup_rng, intros t ht, cases ht with i hi, rw hi, apply continuous_induced_rng, exact H i, end

#### Patrick Massot (May 23 2018 at 12:44):

Out of curiosity, I also tried to build a term proof, but haven't succeeded because of the mysterious rewrite in the middle (which rewrites implicit arguments, which has the weird effect of not changing the visible goal)

#### Patrick Massot (May 23 2018 at 12:45):

I can't get more obfuscated than:

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_Sup_rng $ λ t ht, match ht with ⟨i, hi⟩ := by rw hi ; apply continuous_induced_rng ; exact (H i) end

#### 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*} [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β] {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, exact continuous_add (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*} [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β] {f : γ → α → β} (s : multiset γ) : (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).sum) := quot.induction_on s $ by simp; exact continuous_list_sum lemma continuous_finset_sum {α : Type*} {β : Type*} {γ : Type*} [topological_space α] [topological_space β] [add_comm_monoid β] [topological_add_monoid β] (f : γ → α → β) (s : finset γ) : (∀c∈s, continuous (f c)) → continuous (λa, s.sum (λc, f c a)) := continuous_multiset_sum _

#### Johan Commelin (May 23 2018 at 12:50):

@Patrick Massot Yes, you are completely right. But it seems the work is now already done (-;

#### Mario Carneiro (May 23 2018 at 12:57):

you can see how Johannes built the term proof for `pi_mk`

; the key is to use `continuous_supr_rng`

not `continuous_Sup_rng`

because the definition uses `supr`

(the indexed supremum) not `Sup`

(the set supremum). In fact `supr`

is defined in terms of `Sup`

, but if you apply the wrong theorem it unfolds this definition and things get harder.

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

Yes, I will take a closer look. I think I can learn a lot from how Johannes improved my kludge

#### Patrick Massot (May 23 2018 at 13:13):

Sure. But this is too efficient in a sense. My message was focused on easy local clean up, that you can actually do without any understanding of the proof. Of course this is only the first step. Really efficient proofs like Johannes' require actual thinking

#### Mario Carneiro (May 23 2018 at 13:15):

you can also look at my term proof of `continuous_supr_rng`

, which uses the `\t`

for rewriting

#### Patrick Massot (May 23 2018 at 13:17):

I'm a bit frustrated by this \t thing. I know it's somehow the term version of `rw`

and I see it everywhere in mathlib, but I was almost never able to use it

#### Mario Carneiro (May 23 2018 at 13:17):

I admit it was a bit delicate for me at first

#### Mario Carneiro (May 23 2018 at 13:18):

it is so much weaker than the lean 2 version, it fails whenever the expected type or the thing to rewrite with has metavariables

#### Johan Commelin (May 23 2018 at 13:19):

Anyway, I just proved that the face map between standard simplices is continuous!

#### Johan Commelin (May 23 2018 at 13:19):

The proof is not cleaned up. But it works (-;

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

but it's often just the thing when you want to rewrite with an equality in the context

#### Patrick Massot (May 23 2018 at 13:23):

What about my attempt? Can you use \t there? (without switching to `continuous_supr_rng`

)

#### Mario Carneiro (May 23 2018 at 13:24):

yes, the proof should be almost identical to the one I pointed at

#### Johan Commelin (May 23 2018 at 13:25):

Ok, like I said, the proofs are still ugly. But here goes nothing: https://github.com/jcommelin/mathlib/commit/fec9db2028bea163352f574055dad44029d04788

#### Mario Carneiro (May 23 2018 at 13:25):

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_Sup_rng $ assume t ⟨i, e⟩, e.symm ▸ continuous_induced_rng (H i)

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