English
For a nonempty finite set s and a family f_i, if Tendsto holds for each i ∈ s, then a certain function a ↦ s.inf' hne (f · a) tends to s.inf' hne g.
Русский
Для непустого конечного множества s и семейства f_i, если для каждого i ∈ s выполняется Tendsto, то отображение a ↦ s.inf' hne (f · a) сходится к s.inf' hne g.
LaTeX
$$$\\text{Nonempty}(s) \\Rightarrow (\\forall i \\in s, \\text{Tendsto}(f_i) l (\\mathcal{N}(g_i))) \\Rightarrow \\text{Tendsto}(a \\mapsto s.\\mathrm{inf}' hne (f \\cdot a)) l (\\mathcal{N}(s.\\mathrm{inf}' hne g))$$$
Lean4
theorem finset_inf'_nhds_apply [SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty)
(hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (fun a ↦ s.inf' hne (f · a)) l (𝓝 (s.inf' hne g)) :=
finset_sup'_nhds_apply (L := Lᵒᵈ) hne hs
