finset_inf'_apply — Mathlib

English

Let s be a nonempty finite set and f : ι → X → L with ContinuousOn on t for each i ∈ s. Then the map a ↦ s.inf' hne (f · a) is ContinuousOn t.

Русский

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

LaTeX

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

Lean4

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

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