Theorems · Definition · convex and discrete geometry

gaugeRescale

{E : Type u_1} → [inst : AddCommGroup E] → [Module ℝ E] → Set E → Set E → E → E

The gauge rescale map gaugeRescale s t sends each point x to the point y on the same ray that has the same gauge w.r.t. t as x has w.r.t. s. The characteristic property is satisfied if gauge t x ≠ 0, see gauge_gaugeRescale'. In particular, it is satisfied for all x, provided that t is absorbent and von Neumann bounded.

Defined in

Mathlib.Analysis.Convex.GaugeRescale

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule