We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b191831 commit 8275649Copy full SHA for 8275649
theories/kernel.v
@@ -166,7 +166,8 @@ HB.mixin Record Kernel_isSFinite_subdef d d'
166
167
HB.structure Definition SFiniteKernel d d'
168
(X : measurableType d) (Y : measurableType d') (R : realType) :=
169
- { k of @Kernel _ _ _ _ R k & Kernel_isSFinite_subdef _ _ X Y R k }.
+ { k of @Kernel _ _ _ _ R k &
170
+ Kernel_isSFinite_subdef _ _ X Y R k }.
171
Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X Y R).
172
Arguments sfinite_kernel_subdef {_ _ _ _ _} _.
173
0 commit comments