tendsto_of_antitone — Mathlib

English

A duplicate asserting InfConvergenceClass for the product ι → α.

Русский

Дубликат утверждения о InfConvergenceClass для произведения пространств.

LaTeX

$$$ \InfConvergenceClass(\alpha \times \beta) $$$

Lean4

theorem tendsto_of_antitone {ι α : Type*} [Preorder ι] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α]
    [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : Tendsto f atTop atBot ∨ ∃ l, Tendsto f atTop (𝓝 l) :=
  @tendsto_of_monotone ι αᵒᵈ _ _ _ _ _ h_mono

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