map_isLeast — Mathlib

English

A monotone map sends a least element of a set to a least element of its image.

Русский

Монотонное отображение переводит наименьший элемент множества в наименьший элемент его образа.

LaTeX

$$$\text{MonotoneOn}(f,t) \; \land \; \text{IsLeast}(t,a) \Rightarrow \text{IsLeast}(f''t, f(a))$$$

Lean4

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

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