mathlib3

0d5bfd7b - feat(*): add a few lemmas about `function.extend` (#11498)

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.