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

Русский

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

LaTeX

$$IsLUB(f^{-1}′ s) x ↔ IsLUB(s) (f x)$$

Lean4

@[simp]
theorem isLUB_preimage {s : Set β} {x : α} : IsLUB (f ⁻¹' s) x ↔ IsLUB s (f x) := by
  rw [← f.symm_symm, ← image_eq_preimage, isLUB_image]

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

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

Разделы

Аффилиация

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