Fubini's theorem for non-negative or non-positive functions

DOI10.2478/forma-2018-0005zbMath1401.28007OpenAlexW2887941005MaRDI QIDQ1796769

Noboru Endou

Publication date: 17 October 2018

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2018-0005

zbMATH Keywords

extended real-valued non-negative (or non-positive) measurable functionFubini' s theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Measures and integrals in product spaces (28A35)

Related Items (1)

Fubini's theorem

Uses Software

• Isabelle/HOL
• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Four decades of {\textsc{Mizar}}. Foreword
• Product pre-measure
• Fubini's theorem on measure
• On L1 Space Formed by Complex-Valued Partial Functions
• Three Chapters of Measure Theory in Isabelle/HOL
• Mizar: State-of-the-art and Beyond

This page was built for publication: Fubini's theorem for non-negative or non-positive functions