continuity of division

Stream: maths

[Chris Hughes]

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

[Sebastien Gouezel]

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

[Chris Hughes]

Not particularly, I have no preference.

[Reid Barton]

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

[Chris Hughes]

real.continuous.inv seems to do the trick.

[Chris Hughes]

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

[Chris Hughes]

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

[Johan Commelin]

That would be nice. A real_field tactic?

[Johan Commelin]

Or maybe linear_ordered_field or something like that.

[Johan Commelin]

What is the natural structure in which squares are positive?

[Chris Hughes]

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.

[Johan Commelin]

Exactly. So maybe we can just call it rcf

[Chris Hughes]

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

[Johan Commelin]

Ooh, nice