Prove2Me

Chapter A3u

Definition
ChapterA3u

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

definitionsformalizationtimepiece

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

Definition code
import Definitions.Def_ChapterA3
import Definitions.Def_ChapterA3j
import Definitions.Def_ChapterA3n
import Definitions.Def_ChapterA3o
import Definitions.Def_ChapterA3p
import Definitions.Def_ChapterA3q
import Definitions.Def_ChapterA3r
import Mathlib

namespace BookProof.ChapterA3u

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

View graph