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 #
BoundedSub R: a class guaranteeing boundedness of subtraction.
TODO:
- Add bounded multiplication. (So that, e.g., multiplication works in
X →ᵇ ℝ≥0.)
Bounded subtraction #
A typeclass saying that (p : R × R) ↦ p.1 - p.2 maps any pair of bounded sets to a bounded
set. This property automatically holds for seminormed additive groups, but it also holds, e.g.,
for ℝ≥0.
- isBounded_sub : ∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t)
Instances
theorem
BoundedSub.isBounded_sub
{R : Type u_1}
[Bornology R]
[Sub R]
[self : BoundedSub R]
{s : Set R}
{t : Set R}
:
Bornology.IsBounded s → Bornology.IsBounded t → Bornology.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)
:
Bornology.IsBounded (s - t)
theorem
sub_bounded_of_bounded_of_bounded
{R : Type u_1}
{X : Type u_2}
[PseudoMetricSpace R]
[Sub R]
[BoundedSub R]
{f : X → R}
{g : X → R}
(f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C)
(g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C)
:
Bounded operations in seminormed additive commutative groups #
theorem
SeminormedAddCommGroup.lipschitzWith_sub
{R : Type u_1}
[SeminormedAddCommGroup R]
:
LipschitzWith 2 fun (p : R × R) => p.1 - p.2