toENNReal_max

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_max

English

The embedding preserves max: image of max(m,n) equals max of images.

Русский

Встраивание сохраняет максимум: образ max(m,n) равен max образов.

LaTeX

$$$\\uparrow(\\max(m,n)) = \\max(m,n) \\text{ in } \\mathbb{R}_{\\ge 0,\\infty}.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_max (m n : ℕ∞) : ↑(max m n) = (max m n : ℝ≥0∞) :=
  toENNReal_mono.map_max

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

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

Разделы

Аффилиация

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