OAI/Analysis/LipschitzHilbert/Trees/UnaryRuns.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual consecutive unary runs and their interruption endpoints.

  1. structure OAI.LipschitzHilbert.UnaryRunPartition line 11
  2. theorem OAI.LipschitzHilbert.UnaryRunPartition.separated line 22
  3. theorem OAI.LipschitzHilbert.UnaryRunPartition.end_injective line 42
  4. theorem OAI.LipschitzHilbert.UnarySegmentPartition.end_injective line 55
  5. theorem OAI.LipschitzHilbert.exists_unary_run_end line 66
  6. theorem OAI.LipschitzHilbert.exists_unary_run_partition line 92

    Source documentation

    Consecutive runs are constructed from the predicate itself, including their first nonunary interruption or the final path endpoint.

    theorem exists_unary_run_partition (unary : ℕ → Prop) (start finish : ℕ)
    (horder : start ≤ finish) : Nonempty (UnaryRunPartition unary start finish) := by
…

    Mentions: OAI.LipschitzHilbert.UnaryRunPartition