maximal_mem_image — Mathlib

English

Let f be an order-embedding and x maximal in s. Then f(x) is maximal in f''s.

Русский

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

LaTeX

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

Lean4

theorem maximal_mem_image (f : α ↪o β) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x) :=
  _root_.maximal_mem_image_monotone (by simp [f.le_iff_le]) hx

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