Documentation

Lean 4 Proof

axiom kolmogorov_nagumo (J : ℕ) (F : AggFun J)
    (hcont : IsContinuousAgg J F)
    (hsymm : IsSymmetric J F)
    (hincr : IsStrictlyIncreasing J F)
    (hassoc : IsScaleConsistent J F) :
    IsQuasiArithMean J F

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:192

Module Section

## Emergent CES: Classical Axioms and Main Theorem

In the same file