Where to find a proof about sequential con in mathlib ?

Stream: new members

[Kyle Yank]

image.png

[Kyle Yank]

I want to find the proof of sequential continuity in mathlib. Where should I go?

[Kyle Yank]

Since I haven't found it in the book MIL.

[Kyle Yank]

I want to learn some basic tactics in analysis so that I can write a proof about this theorem in VScode.

[Riccardo Brasca]

The theorem that a function is continuous if and only if it is sequentially continuous (under the appropriate assumptions) is docs#continuous_iff_seqContinuous. Note that the code in your picture is Lean3 code, that is now deprecated.

[Patrick Massot]

The Lean 4 version of this code can be found at https://github.com/PatrickMassot/verbose-lean4

[Kyle Yank]

Thanks a lot.

[Kyle Yank]

Thank you. I'll check it right now.