upperBounds_image — Mathlib

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

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