numeric_congr

Mathlib.SetTheory.Surreal.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.Relabelling.numeric_congr

← MathLib Explorer

English

If x and y are numeric and x ⧏ y, then x < y.

Русский

Если x и y числовые и x ⧏ y, то x < y.

LaTeX

$$$x \lt y$ при условии $x \mathbf{LF} y$ и $x,y$ числовые$$

Lean4

/-- Relabellings preserve being numeric. -/
theorem numeric_congr {x y : PGame} (r : x ≡r y) : Numeric x ↔ Numeric y :=
  ⟨r.numeric_imp, r.symm.numeric_imp⟩

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

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

Разделы

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

Аффилиация

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