inv

Mathlib.Algebra.Order.Group.Pointwise.Bounds

URI: https://scilib.ai/kg/mathlib#IsLUB.inv

English

IsLUB of the inverse set at a, equivalently IsGLB of the original at a.

Русский

IsLUB множества обратного порядка в точке a эквивалентно IsGLB исходного множества при a.

LaTeX

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

Lean4

@[to_additive]
theorem inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ :=
  isGLB_inv'.2 h

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

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

Разделы

Аффилиация

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