finset_inf' — Mathlib

English

For a nonempty finite set s, the map x ↦ s.inf' hne f is ContinuousOn t if all f_i are ContinuousOn t.

Русский

Для непустого конечного s отображение x ↦ 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, Continuous (f i)) : Continuous (s.inf' hne f) :=
  continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf' _ fun i hi ↦ (hs i hi).continuousAt

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