`IndisputableMonolith.CondensedMatter.GlassTransitionStructure`

IndisputableMonolith/CondensedMatter/GlassTransitionStructure.lean · 22 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.CondensedMatter.HighTcSuperconductivityStructure
   3
   4namespace IndisputableMonolith
   5namespace CondensedMatter
   6namespace GlassTransitionStructure
   7
   8open HighTcSuperconductivityStructure
   9
  10def glass_transition_from_ledger : Prop := high_tc_superconductivity_from_ledger
  11
  12theorem glass_transition_structure : glass_transition_from_ledger := high_tc_superconductivity_structure
  13
  14/-- Glass-transition structure implies High-Tc structural input. -/
  15theorem glass_transition_implies_high_tc (h : glass_transition_from_ledger) :
  16    high_tc_superconductivity_from_ledger :=
  17  h
  18
  19end GlassTransitionStructure
  20end CondensedMatter
  21end IndisputableMonolith
  22

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