finset_sup_apply

Mathlib.Topology.Order.Lattice

URI: https://scilib.ai/kg/mathlib#ContinuousOn.finset_sup_apply

← MathLib Explorer

English

For an open set s, s ∈ 𝓝 x iff x ∈ s.

Русский

Для открытого множества s верно: s ∈ 𝓝 x ⇔ x ∈ s.

LaTeX

$$$s \\in \\mathcal{N}(x) \\iff x \\in s$ (для открытого s)$$

Lean4

theorem finset_sup_apply (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (fun a ↦ s.sup (f · a)) t := fun x hx ↦
  ContinuousWithinAt.finset_sup_apply fun i hi ↦ hs i hi x hx

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru