# Images of upper/lower bounds under monotone functions #

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

source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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.

source
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.

source
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.

source
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.

source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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.

source
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.

source
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.

source
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.

source
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)
source
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)
source
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)
source
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)
source
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`.

source
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`.

source
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.

source
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.

source
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)
source
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)
source
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)
source
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)
source
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.

source
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.

source
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.

source
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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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`.

source
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`.

source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
theorem bddAbove_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} :
BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)
source
theorem bddBelow_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set (α × β)} :
BddBelow s ↔ BddBelow (Prod.fst '' s) ∧ BddBelow (Prod.snd '' s)
source
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))
source
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))
source
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
source
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
source
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))
source
theorem bddAbove_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} :
BddAbove s ↔ ∀ (a : α), BddAbove (Function.eval a '' s)
source
theorem bddBelow_pi {α : Type u} {π : α → Type u_1} [(a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} :
BddBelow s ↔ ∀ (a : α), BddBelow (Function.eval a '' s)
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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)
source
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)
source
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))
source
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))