map_isGreatest — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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