iUnion_Ici_eq_Ioi_of_lt_of_tendsto

English

If a < f i for all i and f tends to a, then the union of Ici(f i) equals Ioi(a).

Русский

Если a < f i для всех i и f стремится к a, то объединение Ici(f i) равняется Ioi(a).

LaTeX

$$$ (\forall i, a < f i) \rightarrow Tendsto f F (nhds a) \rightarrow ⋃ i, Ici(f i) = Ioi(a) $$$

Lean4

theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hlt : ∀ i, a < f i) (hlim : Tendsto f F (𝓝 a)) :
    ⋃ i : ι, Ici (f i) = Ioi a :=
  iUnion_Iic_eq_Iio_of_lt_of_tendsto (α := αᵒᵈ) hlt hlim

Похожие утверждения