le_u_l_trans — Mathlib

English

The composition u ∘ l ∘ u equals u for all inputs, i.e., u(l(u(b))) = u(b).

Русский

Состав u ∘ l ∘ u равен u для любых b: u(l(u(b))) = u(b).

LaTeX

$$$\forall b:\; u(l(u(b))) = u(b)$$$

Lean4

/-- If `(l, u)` is a Galois connection, then the relation `x ≤ u (l y)` is a transitive relation.
If `l` is a closure operator (`Submodule.span`, `Subgroup.closure`, ...) and `u` is the coercion to
`Set`, this reads as "if `U` is in the closure of `V` and `V` is in the closure of `W` then `U` is
in the closure of `W`". -/
theorem le_u_l_trans {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z) :=
  hxy.trans (gc.monotone_u <| gc.l_le hyz)

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