finset_inf_apply — Mathlib

English

For nonempty s, if all i ∈ s have ContinuousOn (f i) t, then the map a ↦ s.inf' hne (f · a) is ContinuousOn t.

Русский

Для непустого s, если все i ∈ s имеют ContinuousOn (f i) t, то 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_apply (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (fun a ↦ s.inf (f · a)) t := fun x hx ↦
  ContinuousWithinAt.finset_inf_apply fun i hi ↦ hs i hi x hx

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