max

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#Continuous.max

← MathLib Explorer

English

The maximum of two continuous functions is continuous.

Русский

Максимум двух непрерывных функций — непрерывен.

LaTeX

$$$\text{Continuous }f \land \text{Continuous }g \Rightarrow \text{Continuous}(x \mapsto \max\{f(x), g(x)\}).$$$

Lean4

@[continuity, fun_prop]
protected theorem max (hf : Continuous f) (hg : Continuous g) : Continuous fun b => max (f b) (g b) :=
  Continuous.min (α := αᵒᵈ) hf hg

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

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

Разделы

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

Аффилиация

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