eq_of_forall_gt_iff

Mathlib.Order.Basic

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

English

If, for all c, a < c ↔ b < c, then a = b.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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