finset_inf — Mathlib

English

Let s be nonempty, and f : X → L with each f_i ContinuousOn on t; then a ↦ s.inf' hne f is ContinuousOn t.

Русский

Пусть s непусто и f i : X → L непрерывны на t; тогда a ↦ s.inf' hne f непрерывно на t.

LaTeX

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

Lean4

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

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