pith. machine review for the scientific record. sign in
theorem proved term proof

forall_iff_list

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  43theorem forall_iff_list (P : ℝ → Prop) (m : LeptonMassRatios) :
  44    m.Forall P ↔ ∀ r ∈ m.toList, P r := by

proof body

Term-mode proof.

  45  simp only [Forall, toList, List.mem_cons, List.mem_nil_iff, or_false]
  46  constructor
  47  · rintro ⟨h1, h2, h3⟩ r (rfl | rfl | rfl) <;> assumption
  48  · intro h
  49    exact ⟨h _ (Or.inl rfl), h _ (Or.inr (Or.inl rfl)), h _ (Or.inr (Or.inr rfl))⟩
  50

depends on (6)

Lean names referenced from this declaration's body.