finset_inf'_nhds — Mathlib

English

Let s be a nonempty finite set. If each f_i tends to g_i, then a finite infimum over i of f_i tends to the finite infimum over i of g_i.

Русский

Пусть s — непустое конечное множество; если каждый f_i сходится к g_i, то infimum по i в s сходится к infimum по i в s.

LaTeX

$$$\\text{Nonempty}(s) \\Rightarrow (\\forall i \\in s, \\text{Tendsto}(f_i) l (\\mathcal{N}(g_i))) \\Rightarrow \\text{Tendsto}(s.\\mathrm{inf}' hne f) l (\\mathcal{N}(s.\\mathrm{inf}' hne g))$$$

Lean4

theorem finset_inf'_nhds [SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty)
    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (s.inf' hne f) l (𝓝 (s.inf' hne g)) :=
  finset_sup'_nhds (L := Lᵒᵈ) hne hs

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