finset_inf_apply — Mathlib

English

Let s be a finite nonempty set, and f_i : X → L with ContinuousAt (f_i) x for all i ∈ s. Then the map a ↦ s.inf' hne (f · a) is ContinuousAt at x.

Русский

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

LaTeX

$$$(\text{hne} : s.Nonempty) \rightarrow (\forall i \in s,\ ContinuousAt (f i) x) \rightarrow \text{ContinuousAt}(a \mapsto s.inf' hne (f · a)) x.$$$

Lean4

theorem finset_inf_apply (hs : ∀ i ∈ s, ContinuousAt (f i) x) : ContinuousAt (fun a ↦ s.inf (f · a)) x :=
  Tendsto.finset_inf_nhds_apply hs

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