`IndisputableMonolith.Engineering.TeslaTurbineStructure`

IndisputableMonolith/Engineering/TeslaTurbineStructure.lean · 23 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Engineering.EnergyStorageDensityStructure
   3
   4namespace IndisputableMonolith
   5namespace Engineering
   6namespace TeslaTurbineStructure
   7
   8open EnergyStorageDensityStructure
   9
  10def tesla_turbine_from_ledger : Prop := energy_storage_density_from_ledger
  11
  12theorem tesla_turbine_structure : tesla_turbine_from_ledger :=
  13  energy_storage_density_structure
  14
  15/-- Tesla-turbine structure implies energy-storage-side structural input. -/
  16theorem tesla_turbine_implies_energy_storage (h : tesla_turbine_from_ledger) :
  17    energy_storage_density_from_ledger :=
  18  h
  19
  20end TeslaTurbineStructure
  21end Engineering
  22end IndisputableMonolith
  23

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