continuous_max

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#continuous_max

English

The map (a,b) ↦ max(a,b) from α×α to α is continuous when α is ordered with OrderClosedTopology.

Русский

Отображение (a,b) ↦ max(a,b) непрерывно на α×α при OrderClosedTopology.

LaTeX

$$$\text{Continuous}(p \mapsto \max(p_1,p_2))$ for $p=(p_1,p_2) \in \alpha \times \alpha$.$$

Lean4

theorem continuous_max : Continuous fun p : α × α => max p.1 p.2 :=
  continuous_fst.max continuous_snd

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

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

Разделы

Аффилиация

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