finset_inf' — Mathlib

English

For a nonempty finite s, the function a ↦ s.inf' hne f is ContinuousOn t if each f_i is ContinuousOn t.

Русский

Для непустого конечного s функция a ↦ s.inf' hne f непрерывна на t, если каждый f_i непрерывен на 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' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
    ContinuousWithinAt (s.inf' hne f) t x := by simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

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