filter.at_top for intervals

Stream: Is there code for X?

[Eric Wieser]

We have docs#filter.at_top_Ici_eq for one-sided intervals; is something like the following true for two-sided intervals?

lemma at_top_Ioo (a b : ℝ) :  (at_top : filter (set.Ioo a b)) = (𝓝[≤] b).comap coe :=
sorry

[Jireh Loreaux]

Is it true? Sure, with a hypothesis that a < b. Perhaps you may also prefer to switch 𝓝[≤] to 𝓝[<] in your statement, but I don't think it makes a difference. I'm not sure if we have it though.

[Eric Wieser]

That hypothesis isn't needed:

lemma at_top_Ioo (a b : ℝ) : (filter.at_top : filter (set.Ioo a b)) = (𝓝[≤] b).comap coe :=
begin
  by_cases h : a < b,
  sorry,
  { haveI : is_empty (set.Ioo a b) := set.is_empty_coe_sort.mpr (set.Ioo_eq_empty h),
    simp, },
end

[Jireh Loreaux]

oh duh, sure.

[Yury G. Kudryashov]

We have, e.g., docs#map_coe_Ioo_at_top

[Yury G. Kudryashov]

And docs#comap_coe_Ioo_nhds_within_Iio

[Eric Wieser]

Nice, that looks like exactly what I was looking for. Should we rename either that or at_top_Ici_eq to be more consistent?

[Yury G. Kudryashov]

If you rename it, then you need to switch LHS with RHS.

[Yury G. Kudryashov]

Feel free to do it, but you're forward-porting the changes.

[Yury G. Kudryashov]

The lemmas were added in #5238, then generalized in #5296

[Yury G. Kudryashov]

BTW, #5296 also adds some iff lemmas about tendsto and these filters.

[Eric Wieser]

Which direction do you prefer? (ie, which set of names should we keep?)

[Yury G. Kudryashov]

Sorry, I'm becoming too sleepy to make decisions... When I can't choose, I usually start a vote and let others choose (though it takes a day or two).

[Jireh Loreaux]

I would imagine that docs#filter.at_top_Ici_eq is the more common rewrite direction, but I really don't think it matters much.