# Boundedness in normed groups #

This file rephrases metric boundedness in terms of norms.

## Tags #

normed group

@[simp]
theorem comap_norm_atTop {E : Type u_3} :
Filter.comap norm Filter.atTop =
@[simp]
theorem comap_norm_atTop' {E : Type u_3} [] :
Filter.comap norm Filter.atTop =
theorem Filter.HasBasis.cobounded_of_norm {E : Type u_3} {ι : Sort u_6} {p : ιProp} {s : ι} (h : Filter.atTop.HasBasis p s) :
.HasBasis p fun (i : ι) => norm ⁻¹' s i
theorem Filter.HasBasis.cobounded_of_norm' {E : Type u_3} [] {ι : Sort u_6} {p : ιProp} {s : ι} (h : Filter.atTop.HasBasis p s) :
.HasBasis p fun (i : ι) => norm ⁻¹' s i
theorem Filter.hasBasis_cobounded_norm {E : Type u_3} :
.HasBasis (fun (x : ) => True) fun (x : ) => {x_1 : E | x x_1}
theorem Filter.hasBasis_cobounded_norm' {E : Type u_3} [] :
.HasBasis (fun (x : ) => True) fun (x : ) => {x_1 : E | x x_1}
@[simp]
theorem tendsto_norm_atTop_iff_cobounded {α : Type u_1} {E : Type u_3} {f : αE} {l : } :
Filter.Tendsto (fun (x : α) => f x) l Filter.atTop
@[simp]
theorem tendsto_norm_atTop_iff_cobounded' {α : Type u_1} {E : Type u_3} [] {f : αE} {l : } :
Filter.Tendsto (fun (x : α) => f x) l Filter.atTop
theorem tendsto_norm_cobounded_atTop {E : Type u_3} :
Filter.Tendsto norm Filter.atTop
theorem tendsto_norm_cobounded_atTop' {E : Type u_3} [] :
Filter.Tendsto norm Filter.atTop
theorem eventually_cobounded_le_norm {E : Type u_3} (a : ) :
∀ᶠ (x : E) in , a x
theorem eventually_cobounded_le_norm' {E : Type u_3} [] (a : ) :
∀ᶠ (x : E) in , a x
theorem tendsto_norm_cocompact_atTop {E : Type u_3} [] :
Filter.Tendsto norm () Filter.atTop
theorem tendsto_norm_cocompact_atTop' {E : Type u_3} [] [] :
Filter.Tendsto norm () Filter.atTop
@[simp]
theorem Filter.neg_cobounded {E : Type u_3} :
@[simp]
theorem Filter.inv_cobounded {E : Type u_3} [] :

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity.

theorem Filter.tendsto_inv_cobounded {E : Type u_3} [] :

In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity.

theorem isBounded_iff_forall_norm_le {E : Type u_3} {s : Set E} :
∃ (C : ), xs, x C
theorem isBounded_iff_forall_norm_le' {E : Type u_3} [] {s : Set E} :
∃ (C : ), xs, x C
theorem Bornology.IsBounded.exists_norm_le' {E : Type u_3} [] {s : Set E} :
∃ (C : ), xs, x C

Alias of the forward direction of isBounded_iff_forall_norm_le'.

theorem Bornology.IsBounded.exists_norm_le {E : Type u_3} {s : Set E} :
∃ (C : ), xs, x C

Alias of the forward direction of isBounded_iff_forall_norm_le.

theorem Bornology.IsBounded.exists_pos_norm_le {E : Type u_3} {s : Set E} (hs : ) :
R > 0, xs, x R
abbrev Bornology.IsBounded.exists_pos_norm_le.match_1 {E : Type u_1} {s : Set E} (motive : (∃ (C : ), xs, x C)Prop) :
∀ (x : ∃ (C : ), xs, x C), (∀ (R₀ : ) (hR₀ : xs, x R₀), motive )motive x
Equations
• =
Instances For
theorem Bornology.IsBounded.exists_pos_norm_le' {E : Type u_3} [] {s : Set E} (hs : ) :
R > 0, xs, x R
theorem Bornology.IsBounded.exists_pos_norm_lt {E : Type u_3} {s : Set E} (hs : ) :
R > 0, xs, x < R
abbrev Bornology.IsBounded.exists_pos_norm_lt.match_1 {E : Type u_1} {s : Set E} (motive : (R > 0, xs, x R)Prop) :
∀ (x : R > 0, xs, x R), (∀ (R : ) (hR₀ : R > 0) (hR : xs, x R), motive )motive x
Equations
• =
Instances For
theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_3} [] {s : Set E} (hs : ) :
R > 0, xs, x < R
theorem NormedAddCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_3} [] [] {u : αE} :
ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m - u n < ε
theorem NormedCommGroup.cauchySeq_iff {α : Type u_1} {E : Type u_3} [] [] [] {u : αE} :
ε > 0, ∃ (N : α), ∀ (m : α), N m∀ (n : α), N nu m / u n < ε
theorem IsCompact.exists_bound_of_continuousOn {α : Type u_1} {E : Type u_3} [] {s : Set α} (hs : ) {f : αE} (hf : ) :
∃ (C : ), xs, f x C
theorem IsCompact.exists_bound_of_continuousOn' {α : Type u_1} {E : Type u_3} [] [] {s : Set α} (hs : ) {f : αE} (hf : ) :
∃ (C : ), xs, f x C
theorem HasCompactSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_3} [] {f : αE} (hf : ) (h'f : ) :
∃ (C : ), ∀ (x : α), f x C
theorem HasCompactMulSupport.exists_bound_of_continuous {α : Type u_1} {E : Type u_3} [] [] {f : αE} (hf : ) (h'f : ) :
∃ (C : ), ∀ (x : α), f x C
theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} {f : αE} {g : αF} {l : } (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_one_isBoundedUnder_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [] [] [] {f : αE} {g : αF} {l : } (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∃ (A : ), ∀ (x : E) (y : F), op x y A * x * y) :
Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_zero_isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} {f : αE} {g : αF} {l : } (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_one_isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [] [] [] {f : αE} {g : αF} {l : } (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm g)) (op : EFG) (h_op : ∀ (x : E) (y : F), op x y x * y) :
Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Continuous.bounded_above_of_compact_support {α : Type u_1} {E : Type u_3} [] [] {f : αE} (hf : ) (h : ) :
∃ (C : ), ∀ (x : α), f x C
theorem HasCompactSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_3} [] {f : αE} [Zero E] (hf : ) :
∃ (R : ), 0 < R ∀ (x : α), R xf x = 0
theorem HasCompactMulSupport.exists_pos_le_norm {α : Type u_1} {E : Type u_3} [] {f : αE} [One E] (hf : ) :
∃ (R : ), 0 < R ∀ (x : α), R xf x = 1