map_isGreatest — Mathlib

English

A monotone map preserves least elements: IsLeast s a implies IsLeast (f '' s) (f a).

Русский

Монотонное отображение сохраняет наименьшие элементы: IsLeast s a ⇒ IsLeast (f''s) (f a).

LaTeX

$$$ IsLeast\; s\; a \Rightarrow IsLeast\; (f'' s)\; (f a) $$$

Lean4

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

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