eq_of_forall_lt_iff

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#eq_of_forall_lt_iff

English

If, for every c, c < a is equivalent to c < b, then a = b.

Русский

Если для каждого c верно c < a ⇔ c < b, то a = b.

LaTeX

$$$ (\\\\forall c : \\alpha, c < a \\leftrightarrow c < b) \\Rightarrow a = b $$$

Lean4

theorem eq_of_forall_lt_iff (h : ∀ c, c < a ↔ c < b) : a = b :=
  (le_of_forall_lt fun _ ↦ (h _).1).antisymm <| le_of_forall_lt fun _ ↦ (h _).2

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

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

Разделы

Аффилиация

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