instDistribLatticeCarrier

Mathlib.Order.Category.BddDistLat

URI: https://scilib.ai/kg/mathlib#BddDistLat.instDistribLatticeCarrier

English

Let f be an order isomorphism. Then IsLUB_preimage' holds, reflecting the dual relation with GLB.

Русский

Пусть f — тождественный порядоком изоморфизм. Тогда IsLUB_preimage' отражает двойственную связь с GLB.

LaTeX

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

Lean4

instance (X : BddDistLat) : DistribLattice X :=
  X.toDistLat.str

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

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

Разделы

Аффилиация

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