`IndisputableMonolith.CondensedMatter.RoomTemperatureSuperconductivityStructure`

IndisputableMonolith/CondensedMatter/RoomTemperatureSuperconductivityStructure.lean · 27 lines · 4 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure
   3
   4namespace IndisputableMonolith
   5namespace CondensedMatter
   6namespace RoomTemperatureSuperconductivityStructure
   7
   8open HighTcSuperconductivityStructure
   9
  10theorem has_high_tc_structure : high_tc_superconductivity_from_ledger :=
  11  high_tc_superconductivity_structure
  12
  13def room_temperature_superconductivity_from_ledger : Prop :=
  14  high_tc_superconductivity_from_ledger
  15
  16theorem room_temperature_superconductivity_structure :
  17    room_temperature_superconductivity_from_ledger := has_high_tc_structure
  18
  19/-- Room-temperature-SC structure implies High-Tc structural input. -/
  20theorem room_temperature_implies_high_tc (h : room_temperature_superconductivity_from_ledger) :
  21    high_tc_superconductivity_from_ledger :=
  22  h
  23
  24end RoomTemperatureSuperconductivityStructure
  25end CondensedMatter
  26end IndisputableMonolith
  27

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