Time

In this file we define the time worldvolume as a real line.

Note on implementation

The definition of Time currently inherits all instances of ℝ.

This, in particular, automatically equips Time with a norm. This norm induces a metric on Time which is the standard flat metric. Thus Time automatically corresponds to flat time.

The definition of deriv through fderiv explicitly uses this metric.

Time also inherits instances of ℝ such as a zero vector, the ability to add two time positions etc, which are not really allowed operations on Time.

@[reducible, inline]

abbrev Time : Type

The type Time represents the time manifold.

Equations

• Time = ℝ

noncomputable def Time.deriv {M : Type u_1} [AddCommGroup M] [Module ℝ M] [TopologicalSpace M] (f : Time → M) : Time → M

Given a function f : Time → M the derivative of f.

Equations

• Time.deriv f t = (fderiv ℝ f t) 1

def Time.«term∂ₜ» : Lean.ParserDescr

Given a function f : Time → M the derivative of f.

Equations

• Time.«term∂ₜ» = Lean.ParserDescr.node `Time.«term∂ₜ» 1024 (Lean.ParserDescr.symbol "∂ₜ")