upperBounds_l_image — Mathlib

English

Given a Galois connection between l and u, the upper bounds map via l correspond to upper bounds in the domain, i.e., l maps upper bounds of a set in α to upper bounds of its image in β, and vice versa via u.

Русский

Для Галуа связи между l и u верхние границы множества в α соответствуют верхним границам образа в β через l, и наоборот через u.

LaTeX

$$$$\\operatorname{upperBounds}(l''s) = u^{-1}(\\operatorname{upperBounds}(s))$$$$

Lean4

theorem upperBounds_l_image (s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s :=
  Set.ext fun b => by simp [upperBounds, gc _ _]

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