Filter.map (fun x ↦ c * x)

Stream: Is there code for X?

[Joris van Winden]

Is there an easy way to prove Filter.map (fun x ↦ c * x : ℝ≥0 → ℝ≥0) atTop = atTop? (using 0 < c of course)

I noticed mathlib has Filter.map_add_atTop_eq_nat, but this only works for addition.

[Yury G. Kudryashov]

You can use docs#Filter.map_atTop_eq_of_gc

[Yury G. Kudryashov]

Or docs#OrderIso.map_atTop

[Joris van Winden]

Yury G. Kudryashov said:

You can use docs#Filter.map_atTop_eq_of_gc

Thanks! I got Filter.map_atTop_eq_of_gc_preorder to work in the end