strictMono_l — Mathlib

English

Equivalent statement: using the dual, l ≤ l_ reflection corresponds to u ≤ u_ reflection.

Русский

Эквивалентное утверждение через дуальную форму: соответствие между l и отражением отражено через u.

LaTeX

$$$l(a) \\le l(b) \\text{ iff } a \\le b$$$

Lean4

theorem strictMono_l [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l := fun _ _ h =>
  gi.dual.strictMono_u h

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