From d30caf9f3c3df6de7e26c6c99d2c541fc6cc96b9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 14 Jul 2021 21:26:07 +0900
Subject: [PATCH] definition of measurable function

- from the integral_sketch branch
---
 CHANGELOG_UNRELEASED.md | 2 ++
 theories/measure.v      | 5 +++++
 2 files changed, 7 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 28e2b8126..f5c58612c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -19,6 +19,8 @@
   + lemma `bigcup_set_cond`
 - in `classical_sets.v`:
   + lemmas `bigcupD1`, `bigcapD1`
+- in `measure.v`:
+  + definition `measurable_fun`
 
 ### Changed
 
diff --git a/theories/measure.v b/theories/measure.v
index d7402a4ad..001838ce0 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -41,6 +41,8 @@ From HB Require Import structures.
 (*                        forall Y, mu X = mu (X `&` Y) + mu (X `&` ~` Y)     *)
 (* measure_is_complete mu == the measure mu is complete                       *)
 (*                                                                            *)
+(*     measurable_fun D f == the function f with domain D is measurable       *)
+(*                                                                            *)
 (* Caratheodory theorem:                                                      *)
 (* caratheodory_type mu := T, where mu : {outer_measure set T -> {ereal R}}   *)
 (*                         it is a canonical mesurableType copy of T.         *)
@@ -1035,6 +1037,9 @@ Definition measure_is_complete (R : realType) (T : measurableType)
     (mu : set T -> \bar R) :=
   forall X, mu.-negligible X -> measurable X.
 
+Definition measurable_fun (T U : measurableType) (D : set T) (f : T -> U) :=
+  forall Y, measurable Y -> measurable ((f @^-1` Y) `&` D).
+
 Section caratheodory_measure.
 Variables (R : realType) (T : Type) (mu : {outer_measure set T -> \bar R}).
 Local Notation U := (caratheodory_type mu).