def Function.BoundedBelow {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) : Prop

Equations

• Function.BoundedBelow f = (f '' Set.univ).BoundedBelow

def Function.BoundedAbove {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) : Prop

Equations

• Function.BoundedAbove f = (f '' Set.univ).BoundedAbove

def Function.Bounded {α : Type u_1} {β : Type u_2} [Preorder β] (f : α → β) : Prop

Equations

• Function.Bounded f = (f '' Set.univ).Bounded

@[simp]

theorem Function.boundedBelow_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : α → β} : Function.BoundedBelow f ↔ ∃ (x : β), ∀ (a : α), x ≤ f a

@[simp]

theorem Function.boundedAbove_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : α → β} : Function.BoundedAbove f ↔ ∃ (x : β), ∀ (a : α), f a ≤ x

@[simp]

theorem Function.bounded_iff_above_below {α : Type u_1} {β : Type u_2} [Preorder β] {f : α → β} : Function.Bounded f ↔ Function.BoundedAbove f ∧ Function.BoundedBelow f

theorem Function.bounded_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : α → β} : Function.Bounded f ↔ ∃ (x : β), ∃ (y : β), ∀ (a : α), f a ≤ x ∧ y ≤ f a

theorem Function.BoundedBelow.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} (g : α → β) [Preorder γ] (h : Function.BoundedBelow f) : Function.BoundedBelow (f ∘ g)

theorem Function.BoundedAbove.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} (g : α → β) [Preorder γ] (h : Function.BoundedAbove f) : Function.BoundedAbove (f ∘ g)

theorem Function.Bounded.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} (g : α → β) [Preorder γ] (h : Function.Bounded f) : Function.Bounded (f ∘ g)

theorem boundedBelow_iff_val_boundedBelow {α : Type u_1} [Preorder α] {t : Set α} : t.BoundedBelow ↔ Function.BoundedBelow Subtype.val

theorem boundedAbove_iff_val_boundedAbove {α : Type u_1} [Preorder α] {t : Set α} : t.BoundedAbove ↔ Function.BoundedAbove Subtype.val

theorem bounded_iff_val_bounded {α : Type u_1} [Preorder α] {t : Set α} : t.Bounded ↔ Function.Bounded Subtype.val