Commit 2025-02-15 06:51 e26b4fff
View on Github →chore(Probability/Kernel): add fun_prop attributes, use it (#21861)
I marked measurability lemmas about kernels with fun_prop and used that tactic in various places to replace measurability proofs.
Using fun_prop instead of manual proofs improved some proofs and allowed removing several now unused typeclass arguments.