theorem isBddFun_iff_exists_forall_norm_le' {α : Type u_1} {E : Type u_2} [NormedGroup E] {f : α → E} : Bornology.IsBddFun f ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem isBddFun_iff_exists_forall_norm_le {α : Type u_1} {E : Type u_2} [NormedAddGroup E] {f : α → E} : Bornology.IsBddFun f ↔ ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem Bornology.IsBddFun.exists_forall_norm_le {α : Type u_1} {E : Type u_2} [NormedAddGroup E] {f : α → E} : IsBddFun f → ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

Alias of the forward direction of isBddFun_iff_exists_forall_norm_le.

theorem Bornology.IsBddFun.exists_forall_norm_le' {α : Type u_1} {E : Type u_2} [NormedGroup E] {f : α → E} : IsBddFun f → ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

Alias of the forward direction of isBddFun_iff_exists_forall_norm_le'.

theorem isBddFun_iff_exists_forall_abs_le {α : Type u_1} {f : α → ℝ} : Bornology.IsBddFun f ↔ ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C

theorem Bornology.IsBddFun.exists_forall_abs_le {α : Type u_1} {f : α → ℝ} : IsBddFun f → ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C

Alias of the forward direction of isBddFun_iff_exists_forall_abs_le.