finset_inf' — Mathlib

English

Let s be nonempty and hs : ∀ i ∈ s, ContinuousOn (f i) t. Then ContinuousOn (s.inf' hne f) t.

Русский

Пусть s непусто и для всех i ∈ s отображение f_i непрерывно на t. Тогда 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' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (s.inf' hne f) t :=
  fun x hx ↦ ContinuousWithinAt.finset_inf' hne fun i hi ↦ hs i hi x hx

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