finset_inf — Mathlib

English

If s is nonempty, then for any f: ι → X → L with ContinuousOn (f i) t for i ∈ s, the function a ↦ s.inf' hne (f · a) is ContinuousOn t.

Русский

Пусть s непусто; если f_i непрерывны на t для i ∈ s, то a ↦ s.inf' hne (f · a) непрерывно на t.

LaTeX

$$$(\text{hne} : s.Nonempty) \rightarrow (\forall i \in s,\ \text{ContinuousOn}(f i, t)) \rightarrow \text{ContinuousOn}(a \mapsto s.inf' hne (f \cdot a), t).$$$

Lean4

theorem finset_inf (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.inf f) t x := by
  simpa only [← Finset.inf_apply] using finset_inf_apply hs

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