English
Let α be a topological space that is a complete linear order with the order topology, and let β be a nonempty index set. If f: β → α is Antitone and f(i) tends to a as i tends to atTop (i.e., Tendsto f atTop to nhds a), then the infimum of {f(i) : i ∈ β} equals a.
Русский
Пусть α — полное линейно упорядоченное топологическое пространство с топологией порядка, а β — непустое множество индексов. Пусть f: β → α антинантно (Loe) и f(i) стремится к a по мере i → ∞ (f стремится к a вдоль atTop). Тогда infimum множества {f(i)} по i равен a.
LaTeX
$$$\operatorname{Antitone}(f) \land \operatorname{Tendsto} f \text{ atTop } (\mathcal{N} a) \implies \inf_{i} f(i) = a$$$
Lean4
theorem iInf_eq_of_tendsto {α} [TopologicalSpace α] [CompleteLinearOrder α] [OrderTopology α] [Nonempty β]
[SemilatticeSup β] {f : β → α} {a : α} (hf : Antitone f) : Tendsto f atTop (𝓝 a) → iInf f = a :=
tendsto_nhds_unique (tendsto_atTop_iInf hf)
