const_max

Mathlib.Order.Filter.FilterProduct

URI: https://scilib.ai/kg/mathlib#Filter.Germ.const_max

English

The Germ of the constant maximum equals the maximum of the Germs: const (max x y) = max (const x) (const y).

Русский

Герм константы max x y равен максимуму грамм: const(max x y) = max(const x, const y).

LaTeX

$$$\\mathrm{const}(\\max x y) = \\max(\\mathrm{const}(x),\\mathrm{const}(y)).$$$

Lean4

@[simp]
theorem const_max [LinearOrder β] (x y : β) : (↑(max x y : β) : β*) = max ↑x ↑y := by rw [max_def, map₂_const]

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

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

Разделы

Аффилиация

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