# Zulip Chat Archive

## Stream: maths

### Topic: continuity of division

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

#### Sebastien Gouezel (Jan 23 2020 at 11:29):

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

?

#### Chris Hughes (Jan 23 2020 at 11:33):

Not particularly, I have no preference.

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

#### Chris Hughes (Jan 23 2020 at 11:39):

`real.continuous.inv`

seems to do the trick.

#### Chris Hughes (Jan 23 2020 at 11:39):

But there should probably be a `real.continuous_on_inv`

as well.

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

#### Johan Commelin (Jan 23 2020 at 11:48):

That would be nice. A `real_field`

tactic?

#### Johan Commelin (Jan 23 2020 at 11:48):

Or maybe `linear_ordered_field`

or something like that.

#### Johan Commelin (Jan 23 2020 at 11:50):

What is the natural structure in which squares are positive?

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

#### Johan Commelin (Jan 23 2020 at 12:05):

Exactly. So maybe we can just call it `rcf`

#### Chris Hughes (Jan 23 2020 at 12:06):

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

#### Johan Commelin (Jan 23 2020 at 12:06):

Ooh, nice

Last updated: May 10 2021 at 07:15 UTC