image_setOf_maximal — Mathlib

English

An order-embedding preserves maximality under image.

Русский

Вложение порядка сохраняет максимальность образа.

LaTeX

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

Lean4

theorem image_setOf_maximal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Maximal P x} = {x | Maximal (fun x ↦ P (f.symm x)) x} :=
  by
  convert _root_.image_monotone_setOf_maximal (f := f) (by simp [f.le_iff_le])
  aesop

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