u_le_u_iff

Mathlib.Order.GaloisConnection.Defs

URI: https://scilib.ai/kg/mathlib#GaloisInsertion.u_le_u_iff

← MathLib Explorer

English

For a GaloisInsertion, u preserves and reflects order: u a ≤ u b iff a ≤ b.

Русский

Для GaloisInsertion: u сохраняет и отражает порядок: u a ≤ u b ⇔ a ≤ b.

LaTeX

$$$$ u a \le u b \iff a \le b. $$$$

Lean4

theorem u_le_u_iff [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b} : u a ≤ u b ↔ a ≤ b :=
  ⟨fun h => (gi.le_l_u _).trans (gi.gc.l_le h), fun h => gi.gc.monotone_u h⟩

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

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

Разделы

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

Аффилиация

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