bddBelow_u_image — Mathlib

English

Dual statement to upperBounds_l_image: the lower bounds of the image under u correspond to the preimage under l of the lower bounds.

Русский

Дуальная формулировка: нижние границы образа через u равны предобразу через l нижних границ.

LaTeX

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

Lean4

theorem bddBelow_u_image {s : Set β} : BddBelow (u '' s) ↔ BddBelow s :=
  gc.dual.bddAbove_l_image

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