isGLB_inv'

Mathlib.Algebra.Order.Group.Pointwise.Bounds

URI: https://scilib.ai/kg/mathlib#isGLB_inv'

English

Within IsLUB, inversion sends IsLUB s a to IsGLB s⁻¹ a⁻¹.

Русский

В рамках IsLUB инверсия переводит IsLUB s a в IsGLB s⁻¹ a⁻¹.

LaTeX

$$IsLUB s a \Rightarrow IsGLB s^{-1} a^{-1}$$

Lean4

@[to_additive]
theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a :=
  (OrderIso.inv G).isGLB_preimage'

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

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

Разделы

Аффилиация

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