finset_inf_apply — Mathlib

English

If s is nonempty and each f i is ContinuousOn on t, then the map a ↦ s.inf' hne (f · a) is ContinuousOn t.

Русский

Если s непусто и каждый f_i непрерывен на t, то a ↦ s.inf' hne (f · a) непрерывно на t.

LaTeX

$$(hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (fun a => s.inf' hne (f · a)) t$$

Lean4

theorem finset_inf_apply (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (fun a ↦ s.inf (f · a)) :=
  continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf_apply fun i hi ↦ (hs i hi).continuousAt

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