Documentation

Lean 4 Proof

def IsAggFixedPoint (k : ℕ) (F : AggFun k) : Prop :=
  ∀ (x : Fin k → ℝ), (∀ j, 0 ≤ x j) → aggregationOp k F x = F x

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:33

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file