Questions about IsCoboundedUnder

Stream: new members

[Yongxi Lin (Aaron)]

I am wondering why we need the condition IsCoboundedUnder in the theorem Filter.limsup_le_limsup. If $u\le v$ eventually and we know $v$ is eventually bounded above, then I think it follows that $u$ is eventually bounded above.

Also the theorem isCoboundedUnder_le_of_le says that if a function is bounded from below, then we have IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f. This does not really make sense to me because I believe IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f means that $f$ is frequently bounded from above.

[Aaron Liu]

Yeah I think that can be removed

[Aaron Liu]

Though I don't really understand what docs#Filter.IsCobounded is doing

[Aaron Liu]

For example, is always true when your type has a bottom element, and it's always true when your filter "goes to infinity" in an order without maximal elements

[Yongxi Lin (Aaron)]

Yeah I agree with you. Maybe I should try to formalize Filter.limsup_le_limsup without the IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u assumption? But many theorems in this link https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/LiminfLimsup.html uses the IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u assumption, so I still tend to believe that it is somewhat necessary in this case.

[Aaron Liu]

I can take a look today