finset_inf'_apply — Mathlib

English

For a nonempty finite set s and f_i : X → L, if every f_i is ContinuousWithinAt at x on t, then the function a ↦ s.inf' hne (f · a) is ContinuousWithinAt at x on t.

Русский

Для непустого конечного множества s и функций f_i : X → L, если каждый f_i непрерывно внутри t в точке x, то a ↦ s.inf' hne (f · a) непрерывно внутри t в x.

LaTeX

$$$\text{ContinuousWithinAt}\left(a \mapsto s.inf'\!\ hne\, (f \cdot a),\ t, x\right).$$$

Lean4

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

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