isLUB_image — Mathlib

English

Let f : α ≃o β be an order isomorphism. For any s ⊆ α and x ∈ β, IsLUB(f''s, x) iff IsLUB(s, f.symm x).

Русский

Пусть f : α ≃o β. Тогда IsLUB(f''s, x) эквивалентно IsLUB(s, f.symm x).

LaTeX

$$IsLUB(f''s) x ↔ IsLUB(s) (f.symm x)$$

Lean4

@[simp]
theorem isLUB_image {s : Set α} {x : β} : IsLUB (f '' s) x ↔ IsLUB s (f.symm x) :=
  ⟨fun h => IsLUB.of_image (by simp) ((f.apply_symm_apply x).symm ▸ h), fun h =>
    (IsLUB.of_image (by simp)) <| (f.symm_image_image s).symm ▸ h⟩

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