monotone_l

Mathlib.Order.GaloisConnection.Defs

URI: https://scilib.ai/kg/mathlib#GaloisConnection.monotone_l

English

If x ≤ u(l y) and y ≤ u(l z) then x ≤ u(l z); transitivity in the lifted relation.

Русский

Если x ≤ u(l y) и y ≤ u(l z), то x ≤ u(l z); транситивность связи Галуа на уровне лексической композиции.

LaTeX

$$$\forall x,y,z:\; x \le u(l(y)) \Rightarrow y \le u(l(z)) \Rightarrow x \le u(l(z))$$$

Lean4

theorem monotone_l : Monotone l :=
  gc.dual.monotone_u.dual

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

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

Разделы

Аффилиация

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