finset_inf'_apply — Mathlib

English

Let s be a nonempty finite set of indices, and hs a condition that each f_i is continuous at x. Then the map a ↦ s.inf' hne (f · a) is continuous at x.

Русский

Пусть s непустое конечное множество индексов, и пусть f_i непрерывны в точке x. Тогда отображение a ↦ inf' hne (f · a) непрерывно в x.

LaTeX

$$$\text{ContinuousAt}\left( a \mapsto s.inf'\!\,\text{hne}\, (f \cdot a) , x\right)\quad\text{при условии } (\forall i \in s,\ \text{ContinuousAt}(f_i, x)).$$$

Lean4

theorem finset_inf'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
    ContinuousAt (fun a ↦ s.inf' hne (f · a)) x :=
  Tendsto.finset_inf'_nhds_apply hne hs

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