map_bddBelow — Mathlib

English

If f is monotone and s is bounded below, then the image f''s of s is bounded below by f of a lower bound.

Русский

Если f монотонна и s ограничено снизу, тогда образ f(s) ограничен снизу значением f(C), где C — нижняя граница s.

LaTeX

$$Monotone f → BddBelow s → BddBelow (f '' s)$$

Lean4

/-- The image under a monotone function of a set which is bounded below is bounded below. See also
`BddBelow.image2`. -/
theorem map_bddBelow : BddBelow s → BddBelow (f '' s)
  | ⟨C, hC⟩ => ⟨f C, Hf.mem_lowerBounds_image hC⟩

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