lt_iff_lt

Mathlib.Order.GaloisConnection.Defs

URI: https://scilib.ai/kg/mathlib#GaloisConnection.lt_iff_lt

English

For a Galois connection, b < l(a) iff u(b) < a.

Русский

Для связи Галуа: b < l(a) тогда и только тогда, когда u(b) < a.

LaTeX

$$$$ b < l(a) \iff u(b) < a. $$$$

Lean4

theorem lt_iff_lt (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a :=
  lt_iff_lt_of_le_iff_le (gc a b)

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

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

Разделы

Аффилиация

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