Documentation

Mathlib.Topology.Bornology.BoundedOperation

Bounded operations #

This file introduces type classes for bornologically bounded operations.

In particular, when combined with type classes which guarantee continuity of the same operations, we can equip bounded continuous functions with the corresponding operations.

Main definitions #

Bounded addition #

class BoundedAdd (R : Type u_1) [Bornology R] [Add R] :

A typeclass saying that (p : R × R) ↦ p.1 + p.2 maps any product of bounded sets to a bounded set. This property follows from LipschitzAdd, and thus automatically holds, e.g., for seminormed additive groups.

Instances
    theorem BoundedAdd.isBounded_add {R : Type u_1} :
    ∀ {inst : Bornology R} {inst_1 : Add R} [self : BoundedAdd R] {s t : Set R}, Bornology.IsBounded sBornology.IsBounded tBornology.IsBounded (s + t)
    theorem isBounded_add {R : Type u_1} [Bornology R] [Add R] [BoundedAdd R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) :
    theorem add_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Add R] [BoundedAdd R] {f : XR} {g : XR} (f_bdd : ∃ (C : ), ∀ (x y : X), dist (f x) (f y) C) (g_bdd : ∃ (C : ), ∀ (x y : X), dist (g x) (g y) C) :
    ∃ (C : ), ∀ (x y : X), dist ((f + g) x) ((f + g) y) C

    Bounded subtraction #

    class BoundedSub (R : Type u_1) [Bornology R] [Sub R] :

    A typeclass saying that (p : R × R) ↦ p.1 - p.2 maps any product of bounded sets to a bounded set. This property automatically holds for seminormed additive groups, but it also holds, e.g., for ℝ≥0.

    Instances
      theorem BoundedSub.isBounded_sub {R : Type u_1} :
      ∀ {inst : Bornology R} {inst_1 : Sub R} [self : BoundedSub R] {s t : Set R}, Bornology.IsBounded sBornology.IsBounded tBornology.IsBounded (s - t)
      theorem isBounded_sub {R : Type u_1} [Bornology R] [Sub R] [BoundedSub R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) :
      theorem sub_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Sub R] [BoundedSub R] {f : XR} {g : XR} (f_bdd : ∃ (C : ), ∀ (x y : X), dist (f x) (f y) C) (g_bdd : ∃ (C : ), ∀ (x y : X), dist (g x) (g y) C) :
      ∃ (C : ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) C
      theorem boundedSub_of_lipschitzWith_sub {R : Type u_1} [PseudoMetricSpace R] [Sub R] {K : NNReal} (lip : LipschitzWith K fun (p : R × R) => p.1 - p.2) :

      Bounded multiplication #

      class BoundedMul (R : Type u_1) [Bornology R] [Mul R] :

      A typeclass saying that (p : R × R) ↦ p.1 * p.2 maps any product of bounded sets to a bounded set. This property automatically holds for non-unital seminormed rings, but it also holds, e.g., for ℝ≥0.

      Instances
        theorem BoundedMul.isBounded_mul {R : Type u_1} :
        ∀ {inst : Bornology R} {inst_1 : Mul R} [self : BoundedMul R] {s t : Set R}, Bornology.IsBounded sBornology.IsBounded tBornology.IsBounded (s * t)
        theorem isBounded_mul {R : Type u_1} [Bornology R] [Mul R] [BoundedMul R] {s : Set R} {t : Set R} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) :
        theorem isBounded_pow {R : Type u_2} [Bornology R] [Monoid R] [BoundedMul R] {s : Set R} (s_bdd : Bornology.IsBounded s) (n : ) :
        Bornology.IsBounded ((fun (x : R) => x ^ n) '' s)
        theorem mul_bounded_of_bounded_of_bounded {R : Type u_1} {X : Type u_2} [PseudoMetricSpace R] [Mul R] [BoundedMul R] {f : XR} {g : XR} (f_bdd : ∃ (C : ), ∀ (x y : X), dist (f x) (f y) C) (g_bdd : ∃ (C : ), ∀ (x y : X), dist (g x) (g y) C) :
        ∃ (C : ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) C

        Bounded operations in seminormed additive commutative groups #

        Equations
        • =

        Bounded operations in non-unital seminormed rings #

        Equations
        • =

        Bounded operations in ℝ≥0 #