Real analysis

Stream: new members

[Marcel Hudiani]

Hello, I've been having problems trying to work out a simple limsup, liminf problem involving only sequences in R, at the level of undergraduate mathematics. Is there a workaround in mathlib for limsup/liminfs without having to use filters? I apologize if this is not the correct channel. Please let me know which channel I can ask these types of questions.

[Kenny Lau]

@Marcel Hudiani i'm not a moderator but I think this might belong to #new members (and we can wait for a moderator to move our messages), but in the meantime I can guarantee you that there are standard lemmas to hide all the filters away, such as Filter.limsup_eq and Filter.eventually_atTop.

This is the recommended way to do it, i.e. to use existing very general definitions and then specialise it to your situation. And I really recommend you do it.

But if you really don't want to, you can just define your own limsup functions and provide the basic lemmas to interact with them (i.e. the equivalent of "limsup_eq")

Note that making the right definitions is a non-trivial step in the way to learning Lean, and not everyone may realise that. Having wrong definitions really slows one down.

[Notification Bot]

2 messages were moved here from #Lean for teaching > Real analysis by Bryan Gin-ge Chen.