On 27/07/2020 11:38, Chun Tian (binghe) wrote:
> If f and g are both measurable functions, then {x | f x = g x /\ x IN
> m_space m} (abbrev: {f = g}) must be a measurable set. However, if you
> have just f a measurable function, and {f = g} a measurable set, then it
> is NOT true that g is a measurable set, UNLESS m is a complete measure
> space.
I don't understand that statement at all. Did you mean "it is NOT true
that g is a measurable function"? If yes, then, well, of course not,
since {f = g} could be the empty set (which is certainly measurable) and
then obviously the measurability of f does not tell you anything about
g. Not sure why you are bringing this up.
In any case, all I said in my last email was that you should be able to
easily prove
⊢ ∀a f g h. sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈
Borel_measurable a ⇒ (λx. f x − g x) ∈ Borel_measurable a
no matter what ∞ + -∞ is defined as (including undefined, which is just
some globally fixed value in HOL). But perhaps that is the same
realisation that you also had in your last email.
Manuel
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
