`IndisputableMonolith.Astrophysics.UHECRStructure`

IndisputableMonolith/Astrophysics/UHECRStructure.lean · 21 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Astrophysics
   6namespace UHECRStructure
   7
   8open Constants
   9
  10def uhecr_from_ledger : Prop := 0 < phi
  11
  12theorem uhecr_structure : uhecr_from_ledger := phi_pos
  13
  14/-- UHECR structure implies positivity of `phi`. -/
  15theorem uhecr_implies_phi_pos (h : uhecr_from_ledger) : 0 < phi :=
  16  h
  17
  18end UHECRStructure
  19end Astrophysics
  20end IndisputableMonolith
  21

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