English
Let f : α ≃o β be an order isomorphism. For any subset s ⊆ α, the upper bounds of the image f''s equal the image of the upper bounds: upperBounds(f''s) = f''(upperBounds(s)).
Русский
Пусть f : α ≃o β — тождественный порядоком изоморфизм. Тогда верхние границы образа f''s совпадают с образом верхних границ: upperBounds(f''s) = f''(upperBounds(s)).
LaTeX
$$$upperBounds(f''s) = f''(upperBounds(s)).$$$
Lean4
theorem upperBounds_image {s : Set α} : upperBounds (f '' s) = f '' upperBounds s :=
Subset.antisymm
(fun x hx => ⟨f.symm x, fun _ hy => f.le_symm_apply.2 (hx <| mem_image_of_mem _ hy), f.apply_symm_apply x⟩)
f.monotone.image_upperBounds_subset_upperBounds_image