u_eq_top — Mathlib

English

Let gc be a Galois connection between l and u. For any x ∈ β, u(x) = ⊤ if and only if l(⊤) ≤ x.

Русский

Пусть gc образует связь Галуа между l и u. Для любого x ∈ β верно: u(x) = ⊤ тогда и только тогда, когда l(⊤) ≤ x.

LaTeX

$$$$ u x = \top \iff l(\top) \le x. $$$$

Lean4

theorem u_eq_top {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x} : u x = ⊤ ↔ l ⊤ ≤ x :=
  top_le_iff.symm.trans gc.le_iff_le.symm

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