constants.omdoc
This is a theory containing general physical constants
PhysicalConstants
The vaccuum dielectric permitivity constant (usually denoted by ε_0)
constant vacuum_dielectric_permitivity
type
parsing-notationε_0 (precedence 0)
The elementary charge (denoted by q)
constant elementary_charge
type
parsing-notationq (precedence 0)
The Boltzmann constant (usually denoted by k_B)
constant Boltzmann_constant
type
parsing-notationk_B (precedence 0)
Base
structure PhysicalConstants
domain?PhysicalConstants
structure LFSigma
domain?LFSigma
constant exp
type
constant der
type{P:bool}(((predP))((predP)))
parsing-notationb ' (precedence 0)
constant Real_vec_space2
typetype
definition×
parsing-notationℝ2 (precedence 0)
constant Real_vec_space3
typetype
definition××
parsing-notationℝ3 (precedence 0)
constant comp1
typeℝ3
definition[v:ℝ3](πlv)
constant comp2
typeℝ3
definition[v:ℝ3](πl(πrv))
constant comp3
typeℝ3
definition[v:ℝ3](πr(πrv))
constant pred_as_sub2
type(ℝ2bool)type
definition[P:ℝ2bool]ℝ2|([z:ℝ2]((Pz)))
parsing-notationpred2 a (precedence 0)
constant pred_as_sub3
type(ℝ3bool)type
definition[P:ℝ3bool]ℝ3|([z:ℝ3]((Pz)))
parsing-notationpred3 a (precedence 0)
constant lift_type_one_to_three
type(bool)(ℝ3bool)
definition[P:bool]([v:ℝ3](((P(comp1v))((comp2v)0))((comp3v)0)))
parsing-notationt1↑ a (precedence 0)
constant lift_type_two_to_three
type(ℝ2bool)(ℝ3bool)
definition[P:ℝ2bool]([v:ℝ3]((P(comp1v),(comp2v))((comp3v)0)))
parsing-notationt2↑ a (precedence -1)
constant lift_function_one_to_three
type{P:bool}(((predP))((pred3(t1↑P))))
parsing-notationf1↑ b (precedence 0)
constant lift_function_two_to_three
type{P:ℝ2bool}(((pred2P))((pred3(t2↑P))))
parsing-notationf2↑ b (precedence 0)