lowerBounds_u_image — Mathlib

English

In a Galois connection, the lower bounds behave dually to upper bounds under image maps: the image under u of a set corresponds to the preimage under l of its lower bounds.

Русский

В Гало связи нижние границы ведут себя дуально по отношению к верхним границам подобразам: образ через u множества соответствует предобразу через l нижних граней.

LaTeX

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

Lean4

theorem lowerBounds_u_image (s : Set β) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s :=
  gc.dual.upperBounds_l_image s

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