Mathlib.Order.Bounds.OrderIso

OrderIso.upperBounds_image theorem

{s : Set α} : upperBounds (f '' s) = f '' upperBounds s

Full source

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

Order Isomorphism Preserves Upper Bounds: $\text{upperBounds}(f(s)) = f(\text{upperBounds}(s))$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. Then the set of upper bounds of the image $f(s)$ is equal to the image under $f$ of the set of upper bounds of $s$, i.e., \[ \text{upperBounds}(f(s)) = f(\text{upperBounds}(s)). \]

OrderIso.lowerBounds_image theorem

{s : Set α} : lowerBounds (f '' s) = f '' lowerBounds s

Full source

theorem lowerBounds_image {s : Set α} : lowerBounds (f '' s) = f '' lowerBounds s :=
  @upperBounds_image αᵒᵈ βᵒᵈ _ _ f.dual _

Order Isomorphism Preserves Lower Bounds: $\text{lowerBounds}(f(s)) = f(\text{lowerBounds}(s))$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. Then the set of lower bounds of the image $f(s)$ is equal to the image under $f$ of the set of lower bounds of $s$, i.e., \[ \text{lowerBounds}(f(s)) = f(\text{lowerBounds}(s)). \]

OrderIso.isLUB_image theorem

{s : Set α} {x : β} : IsLUB (f '' s) x ↔ IsLUB s (f.symm x)

Full source

@[simp]
theorem isLUB_image {s : Set α} {x : β} : IsLUBIsLUB (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⟩

Least Upper Bound Preservation under Order Isomorphism: $x = \text{sup}(f(s)) \leftrightarrow f^{-1}(x) = \text{sup}(s)$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. For any $x \in \beta$, $x$ is the least upper bound of the image $f(s)$ if and only if $f^{-1}(x)$ is the least upper bound of $s$.

OrderIso.isLUB_image' theorem

{s : Set α} {x : α} : IsLUB (f '' s) (f x) ↔ IsLUB s x

Full source

theorem isLUB_image' {s : Set α} {x : α} : IsLUBIsLUB (f '' s) (f x) ↔ IsLUB s x := by
  rw [isLUB_image, f.symm_apply_apply]

Least Upper Bound Preservation under Order Isomorphism: $f(\text{sup}(s)) = \text{sup}(f(s))$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. For any $x \in \alpha$, the image $f(x)$ is the least upper bound of the image set $f(s)$ if and only if $x$ is the least upper bound of $s$.

OrderIso.isGLB_image theorem

{s : Set α} {x : β} : IsGLB (f '' s) x ↔ IsGLB s (f.symm x)

Full source

@[simp]
theorem isGLB_image {s : Set α} {x : β} : IsGLBIsGLB (f '' s) x ↔ IsGLB s (f.symm x) :=
  f.dual.isLUB_image

Greatest Lower Bound Preservation under Order Isomorphism: $x = \text{inf}(f(s)) \leftrightarrow f^{-1}(x) = \text{inf}(s)$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. For any $x \in \beta$, $x$ is the greatest lower bound of the image $f(s)$ if and only if $f^{-1}(x)$ is the greatest lower bound of $s$.

OrderIso.isGLB_image' theorem

{s : Set α} {x : α} : IsGLB (f '' s) (f x) ↔ IsGLB s x

Full source

theorem isGLB_image' {s : Set α} {x : α} : IsGLBIsGLB (f '' s) (f x) ↔ IsGLB s x :=
  f.dual.isLUB_image'

Greatest Lower Bound Preservation under Order Isomorphism: $f(\text{inf}(s)) = \text{inf}(f(s))$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \alpha$ be a subset. For any $x \in \alpha$, the image $f(x)$ is the greatest lower bound of the image set $f(s)$ if and only if $x$ is the greatest lower bound of $s$.

OrderIso.isLUB_preimage theorem

{s : Set β} {x : α} : IsLUB (f ⁻¹' s) x ↔ IsLUB s (f x)

Full source

@[simp]
theorem isLUB_preimage {s : Set β} {x : α} : IsLUBIsLUB (f ⁻¹' s) x ↔ IsLUB s (f x) := by
  rw [← f.symm_symm, ← image_eq_preimage, isLUB_image]

Least Upper Bound Preservation under Order Isomorphism Preimage: $\text{sup}(f^{-1}(s)) = x \leftrightarrow \text{sup}(s) = f(x)$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \beta$ be a subset. For any $x \in \alpha$, $x$ is the least upper bound of the preimage $f^{-1}(s)$ if and only if $f(x)$ is the least upper bound of $s$.

OrderIso.isLUB_preimage' theorem

{s : Set β} {x : β} : IsLUB (f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Full source

theorem isLUB_preimage' {s : Set β} {x : β} : IsLUBIsLUB (f ⁻¹' s) (f.symm x) ↔ IsLUB s x := by
  rw [isLUB_preimage, f.apply_symm_apply]

Least Upper Bound Preservation under Order Isomorphism Inverse Preimage: $\text{sup}(f^{-1}(s)) = f^{-1}(x) \leftrightarrow \text{sup}(s) = x$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \beta$ be a subset. For any $x \in \beta$, the inverse image $f^{-1}(x)$ is the least upper bound of the preimage $f^{-1}(s)$ if and only if $x$ is the least upper bound of $s$.

OrderIso.isGLB_preimage theorem

{s : Set β} {x : α} : IsGLB (f ⁻¹' s) x ↔ IsGLB s (f x)

Full source

@[simp]
theorem isGLB_preimage {s : Set β} {x : α} : IsGLBIsGLB (f ⁻¹' s) x ↔ IsGLB s (f x) :=
  f.dual.isLUB_preimage

Greatest Lower Bound Preservation under Order Isomorphism Preimage: $\text{inf}(f^{-1}(s)) = x \leftrightarrow \text{inf}(s) = f(x)$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \beta$ be a subset. For any $x \in \alpha$, $x$ is the greatest lower bound of the preimage $f^{-1}(s)$ if and only if $f(x)$ is the greatest lower bound of $s$.

OrderIso.isGLB_preimage' theorem

{s : Set β} {x : β} : IsGLB (f ⁻¹' s) (f.symm x) ↔ IsGLB s x

Full source

theorem isGLB_preimage' {s : Set β} {x : β} : IsGLBIsGLB (f ⁻¹' s) (f.symm x) ↔ IsGLB s x :=
  f.dual.isLUB_preimage'

Greatest Lower Bound Preservation under Order Isomorphism Inverse Preimage: $\text{inf}(f^{-1}(s)) = f^{-1}(x) \leftrightarrow \text{inf}(s) = x$

Informal description

Let $f : \alpha \simeq_o \beta$ be an order isomorphism between preordered types $\alpha$ and $\beta$, and let $s \subseteq \beta$ be a subset. For any $x \in \beta$, the inverse image $f^{-1}(x)$ is the greatest lower bound of the preimage $f^{-1}(s)$ if and only if $x$ is the greatest lower bound of $s$.