Proof

Stream: new members

[Sovan Sahoo]

example : Tendsto (fun x => sin x / x) (𝓝[≠] 0) (𝓝 1) := by

can anyone get me the tactics to solve this proof in lean4,i am new to lean

[Kevin Buzzard]

First you need to know a maths proof. The tactics you use will depend on which proof you're formalising.

[Weiyi Wang]

Out of curiosity, I went to check how mathlib proved this, and it turns out it doesn't have it? Looks like it is not so important as I thought :sweat_smile:

But mathlib does have a proof of the continuity of the sinc function Real.continuous_sinc, from which one can easily derive the limit

[Kenny Lau]

I think I'll disagree in this instance; this is one of those things that should be in the library instead of requiring one to start with a maths proof

[Kenny Lau]

and in this sentence, after some investigating, it seems like the proved a more general theorem: if f is differentiable at a, then the function (f(b)-f(a))/(b-a) (with f'(a) at a) is continuous at a

[Kenny Lau]

@Sovan Sahoo for the next time, please make a #mwe , i.e. put enough imports and the correct open and also surround your message with triple backticks (```) so that it can be run directly:

import Mathlib

open Real Filter Topology

example : Tendsto sinc (𝓝 0) (𝓝 1) := by
  simpa [ContinuousAt] using continuous_sinc.continuousAt (x := 0)

[Kenny Lau]

```lean4
[code goes here]
```