image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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