`CancerTarget`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.OncologyLattice
domain: CrossDomain
line: 40 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.OncologyLattice on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  37theorem modalityCount : Fintype.card TreatmentModality = 5 := by decide
  38theorem oncogeneCount : Fintype.card OncogeneFamily = 5 := by decide
  39
  40abbrev CancerTarget : Type :=
  41  HallmarkCluster × TreatmentModality × OncogeneFamily
  42
  43theorem cancerTargetCount : Fintype.card CancerTarget = 125 := by
  44  simp only [CancerTarget, Fintype.card_prod,
  45    hallmarkCount, modalityCount, oncogeneCount]
  46
  47theorem hallmark_surj : Function.Surjective (fun t : CancerTarget => t.1) := by
  48  intro x
  49  exact ⟨(x, TreatmentModality.surgery, OncogeneFamily.ras), rfl⟩
  50
  51theorem modality_surj :
  52    Function.Surjective (fun t : CancerTarget => t.2.1) := by
  53  intro x
  54  exact ⟨(HallmarkCluster.proliferation, x, OncogeneFamily.ras), rfl⟩
  55
  56theorem oncogene_surj :
  57    Function.Surjective (fun t : CancerTarget => t.2.2) := by
  58  intro x
  59  exact ⟨(HallmarkCluster.proliferation, TreatmentModality.surgery, x), rfl⟩
  60
  61/-- Multiplicative, not additive: 125 > 15 = 5+5+5. -/
  62theorem product_exceeds_sum :
  63    Fintype.card CancerTarget > Fintype.card HallmarkCluster
  64      + Fintype.card TreatmentModality
  65      + Fintype.card OncogeneFamily := by
  66  rw [cancerTargetCount, hallmarkCount, modalityCount, oncogeneCount]
  67  decide
  68
  69structure OncologyLatticeCert where
  70  target_count : Fintype.card CancerTarget = 125

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.