isLUB_inv'

Mathlib.Algebra.Order.Group.Pointwise.Bounds

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

English

IsLUB of the inverted set at a⁻¹ is equivalent to IsGLB of the original at a.

Русский

IsLUB(Set⁻¹) при a⁻¹ эквивалентно IsGLB исходного множества при a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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