image_of_monotone — Mathlib

English

Let s ⊆ α be partially well-ordered, and f: α → β be monotone. Then the image f[s] is partially well-ordered.

Русский

Пусть s ⊆ α частично хорошо упорядочено, а f: α → β монотонно. Тогда образ f[s] частично хорошо упорядочен.

LaTeX

$$$\\operatorname{IsPWO}(s) \\Rightarrow \\operatorname{Monotone}(f) \\Rightarrow \\operatorname{IsPWO}(f''s)$$$

Lean4

theorem image_of_monotone (hs : s.IsPWO) {f : α → β} (hf : Monotone f) : IsPWO (f '' s) :=
  hs.image_of_monotone_on (hf.monotoneOn _)

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