map_isLeast — Mathlib

English

A monotone map sends a set bounded below to a bounded below image.

Русский

Монотонная отображение переводит множество, ограниченное снизу, в образ под этим отображением, также ограниченный снизу.

LaTeX

$$$ BddBelow\; s \rightarrow BddBelow\; (f '' s) $$$

Lean4

/-- A monotone map sends a least element of a set to a least element of its image. -/
theorem map_isLeast (Ha : IsLeast s a) : IsLeast (f '' s) (f a) :=
  ⟨mem_image_of_mem _ Ha.1, Hf.mem_lowerBounds_image Ha.2⟩

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