Commit 2022-01-17 08:42 0d5bfd7b

feat(*): add a few lemmas about function.extend (#11498) I'm going to use function.extend as another way to get from [encodable ι] (s : ι → set α) to t : ℕ → set α in measure theory.