Documentation

Lean 4 Proof

axiom aczel (J : ℕ) (F : AggFun J)
    (hqa : IsQuasiArithMean J F)
    (hhom : IsHomogDegOne J F) :
    IsPowerMean J F

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:206

Module Section

## Emergent CES: Classical Axioms and Main Theorem

In the same file