bddAbove_l_image — Mathlib

English

Let l and u form a Galois connection; then the set of upper bounds of l''s image equals the preimage under u of upper bounds of s.

Русский

Пусть образ через l задаёт верхние границы; тогда верхние границы образа l''s совпадают с предобразом верхних границ множества s через u.

LaTeX

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

Lean4

theorem bddAbove_l_image {s : Set α} : BddAbove (l '' s) ↔ BddAbove s :=
  ⟨fun ⟨x, hx⟩ => ⟨u x, by rwa [gc.upperBounds_l_image] at hx⟩, gc.monotone_l.map_bddAbove⟩

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