Theorems · Theorem · general topology

add_bounded_of_bounded_of_bounded

∀ {R : Type u_1} {X : Type u_2} [inst : PseudoMetricSpace R] [inst_1 : Add R] [BoundedAdd R] {f g : X → R},
  (∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C) →
    (∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C) → ∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C

Defined in

Mathlib.Topology.Bornology.BoundedOperation

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceAddBoundedAdd