finset_inf_nhds_apply — Mathlib

English

If a finite set s indexes a family f_i, then the map a ↦ s.inf (f_i(a)) tends to s.inf (g_i) under appropriate Tendsto hypotheses.

Русский

Если s индексирует семейство f_i, то отображение a ↦ s.inf (f_i(a)) сходится к s.inf (g_i) при надлежащих условиях сходимости.

LaTeX

$$$\\text{Finset Inf Tendsto Apply}$$$

Lean4

theorem finset_inf_nhds_apply [SemilatticeInf L] [OrderTop L] [ContinuousInf L]
    (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (fun a ↦ s.inf (f · a)) l (𝓝 (s.inf g)) :=
  finset_sup_nhds_apply (L := Lᵒᵈ) hs

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