`mk_toList`

proved

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.ObservablePayloads
domain: RecogSpec
line: 65 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogSpec.ObservablePayloads on GitHub at line 65.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  62  have h3 : a.tau_over_mu = b.tau_over_mu := List.cons.inj (List.cons.inj h23 |>.2) |>.1
  63  exact ext h1 h2 h3
  64
  65@[simp] theorem mk_toList (a b c : ℝ) :
  66    (⟨a, b, c⟩ : LeptonMassRatios).toList = [a, b, c] := rfl
  67
  68end LeptonMassRatios
  69
  70namespace CkmMixingAngles
  71
  72/-- Canonical list view: `[V_us, V_cb, V_ub]`. -/
  73def toList (m : CkmMixingAngles) : List ℝ :=
  74  [m.vus, m.vcb, m.vub]
  75
  76@[simp] theorem toList_length (m : CkmMixingAngles) : m.toList.length = 3 := rfl
  77
  78/-- Every field satisfies a predicate. -/
  79def Forall (P : ℝ → Prop) (m : CkmMixingAngles) : Prop :=
  80  P m.vus ∧ P m.vcb ∧ P m.vub
  81
  82theorem forall_iff_list (P : ℝ → Prop) (m : CkmMixingAngles) :
  83    m.Forall P ↔ ∀ r ∈ m.toList, P r := by
  84  simp only [Forall, toList, List.mem_cons, List.mem_nil_iff, or_false]
  85  constructor
  86  · rintro ⟨h1, h2, h3⟩ r (rfl | rfl | rfl) <;> assumption
  87  · intro h
  88    exact ⟨h _ (Or.inl rfl), h _ (Or.inr (Or.inl rfl)), h _ (Or.inr (Or.inr rfl))⟩
  89
  90@[ext] theorem ext {a b : CkmMixingAngles}
  91    (h1 : a.vus = b.vus)
  92    (h2 : a.vcb = b.vcb)
  93    (h3 : a.vub = b.vub) : a = b := by
  94  cases a; cases b; simp_all
  95

papers checked against this theorem

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