lt_of_lt_of_eq

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.lt_of_lt_of_eq

← MathLib Explorer

English

The product f * inv f hf is equivalent to 1.

Русский

Произведение f на inv f hf эквивалентно 1.

LaTeX

$$$ f \cdot inv\,f\,hf \approx 1 $$$

Lean4

theorem lt_of_lt_of_eq {f g h : CauSeq α abs} (fg : f < g) (gh : g ≈ h) : f < h :=
  show Pos (h - f) by
    convert pos_add_limZero fg (neg_limZero gh) using 1
    simp

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

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

Разделы

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

Аффилиация

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