of_image — Mathlib

English

If f preserves order (hf), then IsLUB of Set.image f s at f x implies IsLUB of s at x.

Русский

Если отображение сохраняет порядок, то верхняя граница образа приводит к верхней границе исходного множества.

LaTeX

$$$ \\IsLUB(\\mathrm{Set.image} f\\ s) (f x) \\Rightarrow \\IsLUB s x $$$

Lean4

theorem of_image [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α}
    (hx : IsLUB (f '' s) (f x)) : IsLUB s x :=
  ⟨fun _ hy => hf.1 <| hx.1 <| mem_image_of_mem _ hy, fun _ hy =>
    hf.1 <| hx.2 <| Monotone.mem_upperBounds_image (fun _ _ => hf.2) hy⟩

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