Documentation

Lean 4 Proof

def IsStrictlyIncreasing (J : ℕ) (F : AggFun J) : Prop :=
  ∀ (x y : Fin J → ℝ), (∀ j, x j ≤ y j) → (∃ j, x j < y j) → F x < F y

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Defs.lean:88

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file