Theorems · Inductive type · general topology

BoundedMul

(R : Type u_1) → [Bornology R] → [Mul R] → Prop

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.

Defined in

Mathlib.Topology.Bornology.BoundedOperation

Cited by

14 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

BornologyMul