Prove2Me

Chapter A3p

Definition
ChapterA3p

by leonardopedro · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

definitionsformalizationtimepiece

Formal definitions for the timepiece Lean 4 formalization (source chapter BookProof/ChapterA3p.lean): generated def bundle for ChapterA3p. See BookProof/ChapterA3p.lean for full context.

Definition code
import Definitions.Def_ChapterA3
import Definitions.Def_ChapterA3j
import Definitions.Def_ChapterA3n
import Definitions.Def_ChapterA3o
import Mathlib

namespace BookProof.ChapterA3p

end BookProof.ChapterA3p
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterA3p.lean

View graph