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