continuity proof

Stream: general

[Reid Barton]

I'm in the process of making continuous into a class and I came across this tricky proof which dates from the creation of mathlib:

lemma continuous_sum_rec {f : α → γ} {g : β → γ}
  (hf : continuous f) (hg : continuous g) : @continuous (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
continuous_sup_dom hf hg

The type of continuous_sup_dom is:

lemma continuous_sup_dom {t₁ t₂ : tspace α} {t₃ : tspace β}
  (h₁ : cont t₁ t₃ f) (h₂ : cont t₂ t₃ f) : cont (t₁ ⊔ t₂) t₃ f

[Reid Barton]

Maybe people will enjoy working out why this proof works.

[Johan Commelin]

Also: it's never used.

[Reid Barton]

I think I use it in lean-homotopy-theory, though (at first I thought maybe I had written it, but no)

[Patrick Massot]

Reid Barton said:

I'm in the process of making continuous into a class and I came across this tricky proof which dates from the creation of mathlib:

Didn't we decide that trying to have the type class system proving stuff for us was a bad idea (at least in Lean3)?

[Reid Barton]

Aah no! I mean a structure!

[Patrick Massot]

Ok. I guess it will break a lot of proofs, but let's see how bad this becomes. I'm ready for changes as long as we don't bundle continuous functions.

[Reid Barton]

It has broken a lot of proofs in minor ways, but now I suddenly encountered a mysterious universe headache

[Patrick Massot]

Clearly you'll have to insert a lot of dots. What do you gain?

[Reid Barton]

apply will work

[Patrick Massot]

Ok, that's a good reason.

[Patrick Massot]

Especially if you then write a continuity tactic