`grLimitRegularityStub`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.NewFixtures
domain: Relativity
line: 169 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.NewFixtures on GitHub at line 169.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

 166-- GRLimitParameterFacts: PROVEN in IndisputableMonolith.Relativity.GRLimit.Parameters
 167-- Instance grLimitParameterFacts_proven is now available; stub removed.
 168
 169noncomputable def grLimitRegularityStub : GRLimitRegularityFacts where
 170  zero_nonsingular := by
 171    intro g ψ vol
 172    exact ⟨by trivial, by intro x; trivial⟩
 173
 174instance : GRLimitRegularityFacts := grLimitRegularityStub

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.