deploy: 1f46280

Author: github-actions

docs/master/mathcomp.analysis.measure_theory.measure_function.html

@@ -346,7 +346,12 @@ <h1 class="title">Module mathcomp.analysis.measure_theory.measure_function</h1>
 &nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#A:5">A</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#f0f4f4a06533e5eeff19ee265a896441"> `|`</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#f0f4f4a06533e5eeff19ee265a896441"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#B:6">B</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
 &nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#A:5">A</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#c7636f45aa1745dbf533da3d408cece1"> `&amp;`</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#c7636f45aa1745dbf533da3d408cece1"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#B:6">B</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> =</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> </a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#set0">set0</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#A:5">A</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#f0f4f4a06533e5eeff19ee265a896441"> `|`</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#f0f4f4a06533e5eeff19ee265a896441"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#B:6">B</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> =</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#A:5">A</a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"> +</a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#B:6">B</a></span>.<br/>
 <br/>
-<span class="vernacular">Definition</span><span class="id"> </span><span id="semi_additive" class="id"><a name="semi_additive" class="" title="semi_additive :
+<span class="vernacular">Definition</span><span class="id"> </span><span id="semi_additive" class="id"><a name="semi_additive" class="" title="ERR:empty response from coq">semi_additive</a></span><span class="id"> :=</span><span class="gallina-kwd"> forall</span><span class="id"> </span><span id="F:7" class="id"><a name="F:7" class="">F</a></span><span class="id"> </span><span id="n:8" class="id"><a name="n:8" class="">n</a></span><span class="id">,</span><br/>
+&nbsp;(<span class="gallina-kwd">forall</span><span class="id"> </span><span id="k:9" class="id"><a name="k:9" class="">k</a></span><span class="id"> :</span><span class="id"> </span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Datatypes.html#nat">nat</a></span><span class="id">,</span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#k:9">k</a></span>))<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> </a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#trivIset">trivIset</a></span><span class="id"> </span><span class="id"><a href="mathcomp.classical.classical_sets.html#setT">setT</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
+&nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">\big[</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#setU">setU</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">/</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#set0">set0</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">]_</a></span>(<span id="k:12" class="id"><span id="k:11" class="id"><span id="k:10" class="id"><a name="k:12" class="">k</a></span></span></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> &lt;</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#k:10">k</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
+&nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span> (<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">\big[</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#setU">setU</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">/</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#set0">set0</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">]_</a></span>(<span id="i:15" class="id"><span id="i:14" class="id"><span id="i:13" class="id"><a name="i:15" class="">i</a></span></span></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> &lt;</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#i:13">i</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> =</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> </a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7">\sum_</a></span>(<span id="i:18" class="id"><span id="i:17" class="id"><span id="i:16" class="id"><a name="i:18" class="">i</a></span></span></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> &lt;</a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#i:16">i</a></span>).<br/>
+<br/>
+<span class="vernacular">Definition</span><span class="id"> </span><span id="semi_sigma_additive" class="id"><a name="semi_sigma_additive" class="" title="semi_additive :
 forall [U V : GRing.BaseAddUMagma.Exports.baseAddUMagmaType],
 (U -> V) -> Prop
 
@@ -355,12 +360,7 @@ <h1 class="title">Module mathcomp.analysis.measure_theory.measure_function</h1>
 semi_additive is transparent
 Expands to: Constant mathcomp.algebra.ssralg.GRing.Theory.semi_additive
 Declared in library mathcomp.algebra.ssralg, line 6909, characters 11-24
-">semi_additive</a></span><span class="id"> :=</span><span class="gallina-kwd"> forall</span><span class="id"> </span><span id="F:7" class="id"><a name="F:7" class="">F</a></span><span class="id"> </span><span id="n:8" class="id"><a name="n:8" class="">n</a></span><span class="id">,</span><br/>
-&nbsp;(<span class="gallina-kwd">forall</span><span class="id"> </span><span id="k:9" class="id"><a name="k:9" class="">k</a></span><span class="id"> :</span><span class="id"> </span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Datatypes.html#nat">nat</a></span><span class="id">,</span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#k:9">k</a></span>))<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> </a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#trivIset">trivIset</a></span><span class="id"> </span><span class="id"><a href="mathcomp.classical.classical_sets.html#setT">setT</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
-&nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">\big[</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#setU">setU</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">/</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#set0">set0</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">]_</a></span>(<span id="k:12" class="id"><span id="k:11" class="id"><span id="k:10" class="id"><a name="k:12" class="">k</a></span></span></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> &lt;</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#k:10">k</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
-&nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span> (<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">\big[</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#setU">setU</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">/</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#set0">set0</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732">]_</a></span>(<span id="i:15" class="id"><span id="i:14" class="id"><span id="i:13" class="id"><a name="i:15" class="">i</a></span></span></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> &lt;</a></span><span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="NOTFOUND the module url for mathcomp.boot.bigop#afef6bddeda988bbc365e556241d5732"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#i:13">i</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> =</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"> </a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7">\sum_</a></span>(<span id="i:18" class="id"><span id="i:17" class="id"><span id="i:16" class="id"><a name="i:18" class="">i</a></span></span></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> &lt;</a></span><span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:8">n</a></span>)<span class="id"><a href="https://math-comp.github.io/htmldoc_2_4_0/mathcomp.algebra.ssralg.html#784f0af919f467115774be372bf0dbd7"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#additivity.mu">mu</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:7">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#i:16">i</a></span>).<br/>
-<br/>
-<span class="vernacular">Definition</span><span class="id"> </span><span id="semi_sigma_additive" class="id"><a name="semi_sigma_additive" class="" title="semi_sigma_additive not a defined object.
+semi_sigma_additive not a defined object.
 ">semi_sigma_additive</a></span><span class="id"> :=</span><br/>
 &nbsp;&nbsp;<span class="gallina-kwd">forall</span><span class="id"> </span><span id="F:19" class="id"><a name="F:19" class="">F</a></span><span class="id">,</span> (<span class="gallina-kwd">forall</span><span class="id"> </span><span id="i:20" class="id"><a name="i:20" class="">i</a></span><span class="id"> :</span><span class="id"> </span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Datatypes.html#nat">nat</a></span><span class="id">,</span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:19">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#i:20">i</a></span>))<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> </a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#trivIset">trivIset</a></span><span class="id"> </span><span class="id"><a href="mathcomp.classical.classical_sets.html#setT">setT</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:19">F</a></span><span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>
 &nbsp;&nbsp;<span class="id"><a href="mathcomp.analysis.measure_theory.measurable_structure.html#measurable">measurable</a></span> (<span class="id"><a href="mathcomp.classical.classical_sets.html#4652af423267d4923a164c1104e1273f">\bigcup_</a></span><span id="n:21" class="id"><a name="n:21" class="">n</a></span><span class="id"><a href="mathcomp.classical.classical_sets.html#4652af423267d4923a164c1104e1273f"> </a></span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#F:19">F</a></span><span class="id"> </span><span class="id"><a href="mathcomp.analysis.measure_theory.measure_function.html#n:21">n</a></span>)<span class="id"><a href="https://rocq-prover.org/corelib/Corelib.Init.Logic.html#::type_scope:x_'-&gt;'_x"> -&gt;</a></span><br/>