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, f.symm x) ↔ IsGLB(s, x).

Русский

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

LaTeX

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

Lean4

theorem isGLB_preimage' {s : Set β} {x : β} : IsGLB (f ⁻¹' s) (f.symm x) ↔ IsGLB s x :=
  f.dual.isLUB_preimage'

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

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

Разделы

Аффилиация

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