of_image — Mathlib

English

If f preserves order (f x ≤ f y iff x ≤ y), then IsGLB of image under f gives IsGLB of the preimage set.

Русский

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

LaTeX

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

Lean4

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

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