finset_inf — Mathlib

English

For a nonempty Finset s, the function x ↦ s.inf' hne f is Continuous on t if each f i is Continuous on t.

Русский

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

LaTeX

$$(hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (x \mapsto s.inf' hne f) .$$

Lean4

theorem finset_inf (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (s.inf f) t := fun x hx ↦
  ContinuousWithinAt.finset_inf fun i hi ↦ hs i hi x hx

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