finset_inf'_apply — Mathlib

English

Let s be finite, and f_i : X → L. If each f_i is Continuous (everywhere), then a ↦ s.inf' hne (f · a) is Continuous.

Русский

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

LaTeX

$$$(\forall i \in s,\ Continuous(f i)) \Rightarrow \text{Continuous}\left(a \mapsto s.inf' hne (f \cdot a)\right).$$$

Lean4

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

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