image_of_monotoneOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_of_monotoneOn (hs : s.IsPWO) {f : α → β} (hf : MonotoneOn f s) : IsPWO (f '' s) :=
  hs.image_of_monotone_on hf

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