image — Mathlib

English

If s is upper and f is an order isomorphism, then the image f(s) is upper.

Русский

Если s — верхнее множество и f — объединённое по порядку отображение, то изображение f(s) верхнее.

LaTeX

$$$IsUpperSet s \\to (f : α \\simeq o\\ β) \\to IsUpperSet (f'' s)$$$

Lean4

theorem image (hs : IsUpperSet s) (f : α ≃o β) : IsUpperSet (f '' s : Set β) :=
  by
  change IsUpperSet ((f : α ≃ β) '' s)
  rw [Set.image_equiv_eq_preimage_symm]
  exact hs.preimage f.symm.monotone

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