Convergence of intervals

If both a and b tend to some filter l₁, sometimes this implies that Ixx a b tends to l₂.lift' powerset, i.e., for any s ∈ l₂ eventually Ixx a b becomes a subset of s. Here and below Ixx is one of Icc, Ico, Ioc, and Ioo. We define filter.tendsto_Ixx_class Ixx l₁ l₂ to be a typeclass representing this property.

The instances provide the best l₂ for a given l₁. In many cases l₁ = l₂ but sometimes we can drop an endpoint from an interval: e.g., we prove tendsto_Ixx_class Ico (𝓟 $ Iic a) (𝓟 $ Iio a), i.e., if u₁ n and u₂ n belong eventually to Iic a, then the interval Ico (u₁ n) (u₂ n) is eventually included in Iio a.

The next table shows “output” filters l₂ for different values of Ixx and l₁. The instances that need topology are defined in topology/algebra/ordered.

| Input filter | Ixx = Icc | Ixx = Ico | Ixx = Ioc | Ixx = Ioo | | -----------: | :-----------: | :-----------: | :-----------: | :-----------: | | at_top | at_top | at_top | at_top | at_top | | at_bot | at_bot | at_bot | at_bot | at_bot | | pure a | pure a | ⊥ | ⊥ | ⊥ | | 𝓟 (Iic a) | 𝓟 (Iic a) | 𝓟 (Iio a) | 𝓟 (Iic a) | 𝓟 (Iio a) | | 𝓟 (Ici a) | 𝓟 (Ici a) | 𝓟 (Ici a) | 𝓟 (Ioi a) | 𝓟 (Ioi a) | | 𝓟 (Ioi a) | 𝓟 (Ioi a) | 𝓟 (Ioi a) | 𝓟 (Ioi a) | 𝓟 (Ioi a) | | 𝓟 (Iio a) | 𝓟 (Iio a) | 𝓟 (Iio a) | 𝓟 (Iio a) | 𝓟 (Iio a) | | 𝓝 a | 𝓝 a | 𝓝 a | 𝓝 a | 𝓝 a | | 𝓝[Iic a] b | 𝓝[Iic a] b | 𝓝[Iio a] b | 𝓝[Iic a] b | 𝓝[Iio a] b | | 𝓝[Ici a] b | 𝓝[Ici a] b | 𝓝[Ici a] b | 𝓝[Ioi a] b | 𝓝[Ioi a] b | | 𝓝[Ioi a] b | 𝓝[Ioi a] b | 𝓝[Ioi a] b | 𝓝[Ioi a] b | 𝓝[Ioi a] b | | 𝓝[Iio a] b | 𝓝[Iio a] b | 𝓝[Iio a] b | 𝓝[Iio a] b | 𝓝[Iio a] b |