`IndisputableMonolith.Nuclear.IslandOfStabilityStructure`

IndisputableMonolith/Nuclear/IslandOfStabilityStructure.lean · 25 lines · 4 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Nuclear.NuclearForceStructure
   3
   4namespace IndisputableMonolith
   5namespace Nuclear
   6namespace IslandOfStabilityStructure
   7
   8open NuclearForceStructure
   9
  10theorem has_nuclear_force_structure : nuclear_force_from_ledger := nuclear_force_structure
  11
  12def island_of_stability_from_ledger : Prop := nuclear_force_from_ledger
  13
  14theorem island_of_stability_structure : island_of_stability_from_ledger :=
  15  has_nuclear_force_structure
  16
  17/-- Island-of-stability structure implies nuclear-force-side input. -/
  18theorem island_of_stability_implies_nuclear_force (h : island_of_stability_from_ledger) :
  19    nuclear_force_from_ledger :=
  20  h
  21
  22end IslandOfStabilityStructure
  23end Nuclear
  24end IndisputableMonolith
  25

source mirrored from github.com/jonwashburn/shape-of-logic