finset_inf — Mathlib

English

Let s be finite and hs i ∈ s implies ContinuousOn (f i) t. Then ContinuousOn (s.inf f) t.

Русский

Пусть s конечен и для каждого i ∈ s отображение f_i непрерывно на t. Тогда s.inf f непрерывно на t.

LaTeX

$$$(\forall i \in s,\ ContinuousOn (f i), t)\Rightarrow \text{ContinuousOn}(s.inf f, t).$$$

Lean4

theorem finset_inf (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.inf f) :=
  continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_inf fun i hi ↦ (hs i hi).continuousAt

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