Documentation

Lean 4 Proof

def aggregationOp (k : ℕ) (f : AggFun k) : AggFun k :=
  fun x => f (fun i => f (fun _j => x i))

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:27

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file