finset_inf' — Mathlib

English

Let s be nonempty; for a family f_i, if all i ∈ s have ContinuousAt at x, then s.inf' hne f is continuous at x.

Русский

Пусть s непусто; если для всех i ∈ s f_i имеют ContinuousAt в x, то s.inf' hne f непрерывно в x.

LaTeX

$$$ (\text{hne} : s.Nonempty) \Rightarrow (\forall i \in s,\ \text{ContinuousAt}(f_i, x)) \Rightarrow \text{ContinuousAt}\bigl(s.inf' \text{hne} f, x\bigr).$ $$

Lean4

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

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