isGLB_preimage

Mathlib.Order.Bounds.OrderIso

URI: https://scilib.ai/kg/mathlib#OrderIso.isGLB_preimage

English

Let f be an order isomorphism. Then IsGLB(f^{-1} s, x) ↔ IsGLB(s, f x).

Русский

Пусть f — тождественный порядоком изоморфизм. Тогда IsGLB(f^{-1} s, x) ↔ IsGLB(s, f x).

LaTeX

$$IsGLB(Set.preimage (RelIso.instFunLike.coe f) s) x ↔ IsGLB s (f x)$$

Lean4

@[simp]
theorem isGLB_preimage {s : Set β} {x : α} : IsGLB (f ⁻¹' s) x ↔ IsGLB s (f x) :=
  f.dual.isLUB_preimage

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

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

Разделы

Аффилиация

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