Commit 2024-09-16 09:18 8192978b

feat: more definitions for the restriction of a dependent function (#16328) If f is a function restricted to a set t and s ⊆ t, define its restriction to s. Add similar definitions with finsets and restrictions to Iic intervals. Prove measurability and continuity.