module
module
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing
show as:
view Lean formalization →
used by (3)
depends on (3)
declarations in this module (11)
-
def
dynamicStructureProfile -
theorem
continuousOn_dynamicStructureProfile -
structure
function -
theorem
concreteDynamicInverseMetric_eq_dynamicStructureProfile -
theorem
concreteDynamicInverseMetric_eq_sample -
def
DynamicWeightedContinuumReach -
theorem
dynamic_weighted_continuum_reach -
theorem
background_weighted_reach_misses_dynamic_family -
theorem
no_fixed_profile_equals_all_dynamic_profiles -
def
TypedResidual_gap5_dynamic_continuum_smearing -
theorem
typedResidual_gap5_dynamic_continuum_smearing