lt_of_lf

Mathlib.SetTheory.Surreal.Basic

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

← MathLib Explorer

English

x ⧏ y if and only if x < y when x,y are numeric.

Русский

x ⧏ y эквивалентно x < y при числовости x и y.

LaTeX

$$$x \mathbf{LF} y \iff x < y$ при числовости $x,y$$$

Lean4

theorem lt_of_lf {x y : PGame} (h : x ⧏ y) (ox : Numeric x) (oy : Numeric y) : x < y :=
  (lt_or_fuzzy_of_lf h).resolve_right (not_fuzzy_of_le (h.le ox oy))

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

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

Разделы

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

Аффилиация

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