u_l_u_eq_u — Mathlib

English

If two Galois connections share the same l, and their u agree on all inputs, then the u-components are equal, i.e., u = u'.

Русский

Если два соединения Галуа имеют одинаковый l и их u совпадают на всех элементах, то u = u'.

LaTeX

$$$\mathrm{u_{unique}}:\; \forall l',u',\; (\mathrm{GaloisConnection}\;l'\;u') \to (\forall b:\beta, u b = u'(b)) \Rightarrow \forall b:\beta, u(b)=u'(b)$$

Lean4

theorem u_l_u_eq_u (b : β) : u (l (u b)) = u b :=
  (gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)

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