iUnion_Iic_eq_Iio_of_lt_of_tendsto

English

Let a ∈ α and f: ι → α with ∀ i, f(i) < a and Tendsto f F (nhds a). Then ⋃ i Iic(f(i)) = Iio(a).

Русский

Пусть a ∈ α и f: ι → α так, что ∀ i, f(i) < a и Tendsto f F (nhds a). Тогда ⋃ i Iic(f(i)) = Iio(a).

LaTeX

$$⋃ i: ι, Iic(f(i)) = Iio(a)$$

Lean4

theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hlt : ∀ i, f i < a) (hlim : Tendsto f F (𝓝 a)) :
    ⋃ i : ι, Iic (f i) = Iio a :=
  by
  have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
  rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]

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