eq_of_forall_ge_iff

Mathlib.Order.Basic

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

English

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

Русский

Если для всех c выполняется a ≤ c ⇔ b ≤ c, то a = b.

LaTeX

$$$\\forall c, a \\le c \\leftrightarrow b \\le c \\Rightarrow a = b$$$

Lean4

theorem eq_of_forall_ge_iff (H : ∀ c, a ≤ c ↔ b ≤ c) : a = b :=
  ((H _).2 le_rfl).antisymm ((H _).1 le_rfl)

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

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

Разделы

Аффилиация

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