Prove2Me

`BookProof.ChapterNoBestPrior.distinct_priors_each_preferred` (p q : Hyp → ℝ) (hpq : p ≠ q) : (∃ u, expectedUtility q u < expectedUtility p u) ∧ ∃ v, expectedUtility p v < expected

Proved
BookProof.ChapterNoBestPrior.distinct_priors_each_preferred

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNoBestPrior.

BookProof.ChapterNoBestPrior.distinct_priors_each_preferred (p q : Hyp → ℝ) (hpq : p ≠ q) : (∃ u, expectedUtility q u < expectedUtility p u) ∧ ∃ v, expectedUtility p v < expectedUtility q v

Formalization note: Lean 4 identifier BookProof.ChapterNoBestPrior.distinct_priors_each_preferred.

Preamble
-- Generated from ChapterNoBestPrior.lean — theorem BookProof.ChapterNoBestPrior.distinct_priors_each_preferred
import Mathlib
import Definitions.Def_ChapterNoBestPrior
open BookProof.ChapterNoBestPrior


open scoped BigOperators


variable {Hyp : Type*} [Fintype Hyp]
Formal statement
theorem BookProof.ChapterNoBestPrior.distinct_priors_each_preferred (p q : Hyp → ℝ) (hpq : p ≠ q) :
    (∃ u, expectedUtility q u < expectedUtility p u) ∧
      ∃ v, expectedUtility p v < expectedUtility q v := by sorry

View graph