def
definition
def or abbrev
BoundaryConditions
show as:
view Lean formalization →
formal statement (Lean)
141def BoundaryConditions (metric : StaticSphericalMetric) : Prop :=
proof body
Definition body.
142 (∀ ε > 0, ∃ R, ∀ r > R, |metric.f r - 1| < ε) ∧
143 (∀ ε > 0, ∃ R, ∀ r > R, |metric.g r - 1| < ε)
144
145/-!
146Schwarzschild limit (documentation / TODO).
147
148Intended claim: in the appropriate parameter regime, solutions reduce to the Schwarzschild metric.
149-/
150
151end Compact
152end Relativity
153end IndisputableMonolith