Commit 2026-08-08 15:51 641fbd32

View on Github →

feat(Logic/Function/Defs): add Function.diag (#41082) Adds a name for the function fun x => (x, x).

Estimated changes

modified def Finset.diag
modified theorem Set.diag_image
modified theorem Set.diag_preimage_prod
modified theorem Set.diag_preimage_prod_self
modified theorem Set.diagonal_subset_iff
modified theorem Set.range_diag
added theorem Function.diag_apply
added theorem Function.diag_comp
added theorem Function.diag_def
added theorem Function.fst_comp_diag
added theorem Function.map_comp_diag
added theorem Function.prod_id_id
added theorem Function.snd_comp_diag
added theorem measurable_diag'
added theorem measurable_diag
modified theorem Filter.tendsto_diag
added theorem continuous_diag