finset_inf_apply — Mathlib

English

For a nonempty finite s, the function a ↦ s.inf' hne (f · a) is ContinuousWithinAt t x whenever all f_i are ContinuousWithinAt at x.

Русский

Пусть s непусто; если для всех i ∈ s f_i непрерывны внутри t в x, то a ↦ s.inf' hne (f · a) непрерывно внутри t в x.

LaTeX

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

Lean4

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

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