Commit 2025-01-27 14:13 b849359f

feat: define Descriptive.Tree (#18763) Define trees in the sense of descriptive set theory. Deduce SetLike from a more general instance about complete sublattices of power set lattices. Taken from https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean