Images of upper/lower bounds under monotone functions

In this file we prove various results about the behaviour of bounds under monotone/antitone maps.

theorem MonotoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) (Hat : a ∈ t) : f a ∈ upperBounds (f '' s)

theorem MonotoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

theorem MonotoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) (Hat : a ∈ t) : f a ∈ lowerBounds (f '' s)

theorem MonotoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)

theorem MonotoneOn.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)

theorem MonotoneOn.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)

theorem MonotoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddAbove (f '' s)

The image under a monotone function on a set t of a subset which has an upper bound in t is bounded above.

theorem MonotoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : MonotoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)

The image under a monotone function on a set t of a subset which has a lower bound in t is bounded below.

theorem MonotoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) (Ha : IsLeast t a) : IsLeast (f '' t) (f a)

A monotone map sends a least element of a set to a least element of its image.

theorem MonotoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : MonotoneOn f t) (Ha : IsGreatest t a) : IsGreatest (f '' t) (f a)

A monotone map sends a greatest element of a set to a greatest element of its image.

theorem AntitoneOn.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) (Has : a ∈ lowerBounds s) : a ∈ t → f a ∈ upperBounds (f '' s)

theorem AntitoneOn.mem_upperBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)

theorem AntitoneOn.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} {a : α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)

theorem AntitoneOn.mem_lowerBounds_image_self {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)

theorem AntitoneOn.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)

theorem AntitoneOn.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)

theorem AntitoneOn.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)

The image under an antitone function of a set which is bounded above is bounded below.

theorem AntitoneOn.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {s t : Set α} (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)

The image under an antitone function of a set which is bounded below is bounded above.

theorem AntitoneOn.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a)

An antitone map sends a greatest element of a set to a least element of its image.

theorem AntitoneOn.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {t : Set α} {a : α} (Hf : AntitoneOn f t) : IsLeast t a → IsGreatest (f '' t) (f a)

An antitone map sends a least element of a set to a greatest element of its image.

theorem Monotone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ upperBounds s) : f a ∈ upperBounds (f '' s)

theorem Monotone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : a ∈ lowerBounds s) : f a ∈ lowerBounds (f '' s)

theorem Monotone.image_upperBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' upperBounds s ⊆ upperBounds (f '' s)

theorem Monotone.image_lowerBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : f '' lowerBounds s ⊆ lowerBounds (f '' s)

theorem Monotone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : BddAbove s → BddAbove (f '' s)

The image under a monotone function of a set which is bounded above is bounded above. See also BddAbove.image2.

theorem Monotone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {s : Set α} : BddBelow s → BddBelow (f '' s)

The image under a monotone function of a set which is bounded below is bounded below. See also BddBelow.image2.

theorem Monotone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsLeast s a) : IsLeast (f '' s) (f a)

A monotone map sends a least element of a set to a least element of its image.

theorem Monotone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (Hf : Monotone f) {a : α} {s : Set α} (Ha : IsGreatest s a) : IsGreatest (f '' s) (f a)

A monotone map sends a greatest element of a set to a greatest element of its image.

theorem Antitone.mem_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)

theorem Antitone.mem_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)

theorem Antitone.image_lowerBounds_subset_upperBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' lowerBounds s ⊆ upperBounds (f '' s)

theorem Antitone.image_upperBounds_subset_lowerBounds_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : f '' upperBounds s ⊆ lowerBounds (f '' s)

theorem Antitone.map_bddAbove {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : BddAbove s → BddBelow (f '' s)

The image under an antitone function of a set which is bounded above is bounded below.

theorem Antitone.map_bddBelow {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {s : Set α} : BddBelow s → BddAbove (f '' s)

The image under an antitone function of a set which is bounded below is bounded above.

theorem Antitone.map_isGreatest {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : IsGreatest s a → IsLeast (f '' s) (f a)

An antitone map sends a greatest element of a set to a least element of its image.

theorem Antitone.map_isLeast {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) {a : α} {s : Set α} : IsLeast s a → IsGreatest (f '' s) (f a)

An antitone map sends a least element of a set to a greatest element of its image.

theorem StrictMono.mem_upperBounds_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s

theorem StrictMono.mem_lowerBounds_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s

theorem StrictMono.map_isLeast {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : IsLeast (f '' s) (f a) ↔ IsLeast s a

theorem StrictMono.map_isGreatest {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictMono f) : IsGreatest (f '' s) (f a) ↔ IsGreatest s a

theorem StrictAnti.mem_upperBounds_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s

theorem StrictAnti.mem_lowerBounds_image {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s

theorem StrictAnti.map_isLeast {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : IsLeast (f '' s) (f a) ↔ IsGreatest s a

theorem StrictAnti.map_isGreatest {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] {f : α → β} {a : α} {s : Set α} (hf : StrictAnti f) : IsGreatest (f '' s) (f a) ↔ IsLeast s a

theorem mem_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_upperBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_lowerBounds_subset {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddAbove.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)

See also Monotone.map_bddAbove.

theorem BddBelow.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)

See also Monotone.map_bddBelow.

theorem IsGreatest.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsLeast.image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddAbove.bddAbove_image2_of_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)

theorem BddBelow.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)

theorem IsGreatest.isGreatest_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsLeast.isLeast_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Monotone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_upperBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddBelow.image2_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)

theorem BddAbove.image2_bddBelow {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) : BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)

theorem IsLeast.isGreatest_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsLeast s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsGreatest.isLeast_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Antitone (f a)) (ha : IsGreatest s a) (hb : IsGreatest t b) : IsLeast (Set.image2 f s t) (f a b)

theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds t) : f a b ∈ upperBounds (Set.image2 f s t)

theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : a ∈ upperBounds s) (hb : b ∈ lowerBounds t) : f a b ∈ lowerBounds (Set.image2 f s t)

theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)

theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2 {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)

theorem BddBelow.bddAbove_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)

theorem BddAbove.bddBelow_image2_of_bddAbove {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) : BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)

theorem IsLeast.isGreatest_image2_of_isGreatest {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsLeast s a) (hb : IsGreatest t b) : IsGreatest (Set.image2 f s t) (f a b)

theorem IsGreatest.isLeast_image2_of_isLeast {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (h₀ : ∀ (b : β), Antitone (Function.swap f b)) (h₁ : ∀ (a : α), Monotone (f a)) (ha : IsGreatest s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b)

theorem IsCofinalFor.image_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s t : Set α} {f : α → β} (hst : IsCofinalFor s t) (hf : Monotone f) : IsCofinalFor (f '' s) (f '' t)

theorem IsCofinalFor.image_of_antitone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s t : Set α} {f : α → β} (hst : IsCofinalFor s t) (hf : Antitone f) : IsCoinitialFor (f '' s) (f '' t)

theorem IsCoinitialFor.image_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s t : Set α} {f : α → β} (hst : IsCoinitialFor s t) (hf : Monotone f) : IsCoinitialFor (f '' s) (f '' t)

theorem IsCoinitialFor.image_of_antitone {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s t : Set α} {f : α → β} (hst : IsCoinitialFor s t) (hf : Antitone f) : IsCofinalFor (f '' s) (f '' t)

theorem bddAbove_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} : BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)

theorem bddBelow_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} : BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s)

theorem bddAbove_range_prod {ι : Sort x} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {F : ι → α × β} : BddAbove (Set.range F) ↔ BddAbove (Set.range (Prod.fst ∘ F)) ∧ BddAbove (Set.range (Prod.snd ∘ F))

theorem bddBelow_range_prod {ι : Sort x} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {F : ι → α × β} : BddBelow (Set.range F) ↔ BddBelow (Set.range (Prod.fst ∘ F)) ∧ BddBelow (Set.range (Prod.snd ∘ F))

theorem isLUB_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2

theorem isGLB_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} (p : α × β) : IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2

theorem Monotone.upperBounds_image_of_directedOn_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {γ : Type u_3} [Preorder γ] {g : α × β → γ} (hg : Monotone g) {d : Set (α × β)} (hd : DirectedOn (fun (x1 x2 : α × β) => x1 ≤ x2) d) : upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d))

theorem bddAbove_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} : BddAbove s ↔ ∀ (a : α), BddAbove (Function.eval a '' s)

theorem bddBelow_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} : BddBelow s ↔ ∀ (a : α), BddBelow (Function.eval a '' s)

theorem bddAbove_range_pi {α : Type u} {ι : Sort x} {π : α → Type u_1} [(a : α) → Preorder (π a)] {F : ι → (a : α) → π a} : BddAbove (Set.range F) ↔ ∀ (a : α), BddAbove (Set.range fun (i : ι) => F i a)

theorem bddBelow_range_pi {α : Type u} {ι : Sort x} {π : α → Type u_1} [(a : α) → Preorder (π a)] {F : ι → (a : α) → π a} : BddBelow (Set.range F) ↔ ∀ (a : α), BddBelow (Set.range fun (i : ι) => F i a)

theorem isLUB_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} : IsLUB s f ↔ ∀ (a : α), IsLUB (Function.eval a '' s) (f a)

theorem isGLB_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a} : IsGLB s f ↔ ∀ (a : α), IsGLB (Function.eval a '' s) (f a)

theorem IsGLB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsGLB (f '' s) (f x)) : IsGLB s x

theorem IsLUB.of_image {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} (hf : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) {s : Set α} {x : α} (hx : IsLUB (f '' s) (f x)) : IsLUB s x

theorem BddAbove.range_mono {α : Type u} {β : Type v} [Preorder β] {f : α → β} (g : α → β) (h : ∀ (a : α), f a ≤ g a) (hbdd : BddAbove (Set.range g)) : BddAbove (Set.range f)

theorem BddBelow.range_mono {α : Type u} {β : Type v} [Preorder β] (f : α → β) {g : α → β} (h : ∀ (a : α), f a ≤ g a) (hbdd : BddBelow (Set.range f)) : BddBelow (Set.range g)

theorem BddAbove.range_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : BddAbove (Set.range f)) (hg : Monotone g) : BddAbove (Set.range fun (x : α) => g (f x))

theorem BddBelow.range_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : BddBelow (Set.range f)) (hg : Monotone g) : BddBelow (Set.range fun (x : α) => g (f x))