isLUB_preimage'

Mathlib.Order.Bounds.OrderIso

URI: https://scilib.ai/kg/mathlib#OrderIso.isLUB_preimage'

English

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

Русский

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

LaTeX

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

Lean4

theorem isLUB_preimage' {s : Set β} {x : β} : IsLUB (f ⁻¹' s) (f.symm x) ↔ IsLUB s x := by
  rw [isLUB_preimage, f.apply_symm_apply]

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

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

Разделы

Аффилиация

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