minimal_mem_image — Mathlib

English

Let f be an order-embedding from α to β and x be minimal in s. Then f(x) is minimal in f''s.

Русский

Пусть f — вложение порядка из α в β, и x минимален в s. Тогда f(x) минимален в f''s.

LaTeX

$$$\\forall f:\\, \\alpha \\hookrightarrow\\beta,\; (\\text{Minimal}(\\cdot \\in s) x) \\Rightarrow (\\text{Minimal}(\\cdot \\in f'' s) f(x))$$$

Lean4

theorem minimal_mem_image (f : α ↪o β) (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x) :=
  _root_.minimal_mem_image_monotone (by simp [f.le_iff_le]) hx

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