map_isLeast — Mathlib

English

A strictly monotone map preserves least elements under images, but here relates to greatest to least under anti/monotone context.

Русский

Строго монотонное отображение сохраняет структуру минимальности/максимальности в изображении.

LaTeX

$$IsGreatest(s,a) \rightarrow IsLeast(f''(s)) (f(a))$$

Lean4

/-- An antitone map sends a least element of a set to a greatest element of its image. -/
theorem map_isLeast : IsLeast s a → IsGreatest (f '' s) (f a) :=
  hf.dual_right.map_isLeast

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