TimeLike

Statistics

Metric	Count
Definitions	0
Theorems `timeComponent_squared_pos_of_timelike`, `timeLike_iff_norm_sq_pos`, `timeLike_iff_time_lt_space`, `time_component_ne_zero_of_timelike`, `timelike_neg_time_component_product`, `timelike_spatial_lt_time_squared`, `timelike_time_component_ne_zero`, `timelike_time_dominates_space`	8
Total	8

Name	Kind	Assumes	Proves	Validates	Depends On
`timeComponent_squared_pos_of_timelike` 📖	mathematical	`causalCharacter` `CausalCharacter.timeLike`	`timeComponent`	—	`time_component_ne_zero_of_timelike`
`timeLike_iff_norm_sq_pos` 📖	mathematical	—	`causalCharacter` `CausalCharacter.timeLike` `Lorentz.Vector` `isNormedAddCommGroup` `instAddCommMonoid` `instModuleReal` `instAddCommGroup` `minkowskiProduct`	—	—
`timeLike_iff_time_lt_space` 📖	mathematical	—	`causalCharacter` `CausalCharacter.timeLike` `spatialPart`	—	`minkowskiProduct_toCoord` `timeLike_iff_norm_sq_pos`
`time_component_ne_zero_of_timelike` 📖	—	`causalCharacter` `CausalCharacter.timeLike`	—	—	`minkowskiProduct_toCoord` `timeLike_iff_norm_sq_pos`
`timelike_neg_time_component_product` 📖	—	—	—	—	—
`timelike_spatial_lt_time_squared` 📖	mathematical	`causalCharacter` `CausalCharacter.timeLike`	`spatialPart` `timeComponent`	—	`minkowskiProduct_toCoord` `timeLike_iff_norm_sq_pos`
`timelike_time_component_ne_zero` 📖	—	`causalCharacter` `CausalCharacter.timeLike`	—	—	`time_component_ne_zero_of_timelike`
`timelike_time_dominates_space` 📖	mathematical	`causalCharacter` `CausalCharacter.timeLike`	`spatialPart` `timeComponent`	—	`minkowskiProduct_toCoord` `timeLike_iff_norm_sq_pos`

---