Zulip Chat Archive

Stream: maths

Topic: continuity of division


view this post on Zulip Chris Hughes (Jan 23 2020 at 11:20):

What's the canonical way of stating and proving this? I got stuck on the division.

example : continuous (λ x : { x :  ×  // x  (0, 0) },
  (x.1.1 * x.1.2) / (x.1.1^2 + x.1.2^2)) :=
continuous.mul
  (continuous.mul
    (continuous_fst.comp continuous_subtype_val)
    (continuous_snd.comp continuous_subtype_val))
  begin


  end

view this post on Zulip Sebastien Gouezel (Jan 23 2020 at 11:29):

Do you really want to use a subtype, instead of continuous_on?

view this post on Zulip Chris Hughes (Jan 23 2020 at 11:33):

Not particularly, I have no preference.

view this post on Zulip Reid Barton (Jan 23 2020 at 11:37):

maybe something like

  begin
    let f : { x :  ×  // x  (0, 0) }  { y :  // y  0 } :=
      λ x, x.1.1^2 + x.1.2^2, sorry,
    have : continuous f := continuous_subtype_mk _ sorry,
    exact (show _, from continuous.comp real.continuous_inv this),
  end

view this post on Zulip Chris Hughes (Jan 23 2020 at 11:39):

real.continuous.inv seems to do the trick.

view this post on Zulip Chris Hughes (Jan 23 2020 at 11:39):

But there should probably be a real.continuous_on_inv as well.

view this post on Zulip Chris Hughes (Jan 23 2020 at 11:43):

One day a tactic will do this for me
x₁ x₂ : ℝ, hx : (x₁, x₂) ≠ (0, 0) ⊢ ¬x₁ ^ 2 + x₂ ^ 2 = 0

view this post on Zulip Johan Commelin (Jan 23 2020 at 11:48):

That would be nice. A real_field tactic?

view this post on Zulip Johan Commelin (Jan 23 2020 at 11:48):

Or maybe linear_ordered_field or something like that.

view this post on Zulip Johan Commelin (Jan 23 2020 at 11:50):

What is the natural structure in which squares are positive?

view this post on Zulip Chris Hughes (Jan 23 2020 at 12:04):

The first order theory of real closed fields is decidable. I suppose a tactic that solved that theory could also prove some statements over a subset of a real closed field as well.

view this post on Zulip Johan Commelin (Jan 23 2020 at 12:05):

Exactly. So maybe we can just call it rcf

view this post on Zulip Chris Hughes (Jan 23 2020 at 12:06):

There was a talk about it by Wenda Li at Lean together.

view this post on Zulip Johan Commelin (Jan 23 2020 at 12:06):

Ooh, nice


Last updated: May 10 2021 at 07:15 UTC