const_min

Mathlib.Order.Filter.FilterProduct

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

English

The Germ of the constant minimum equals the minimum of the Germs: const (min x y) = min (const x) (const y).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem const_min [LinearOrder β] (x y : β) : (↑(min x y : β) : β*) = min ↑x ↑y := by rw [min_def, map₂_const]

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

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

Разделы

Аффилиация

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