Not that easy, or just impossible. However, if f and g are positive and
negative parts of the same function (h), then the theorem indeed holds
without any extra antecedents:
[IN_MEASURABLE_BOREL_PLUS_MINUS] Theorem
⊢ ∀a f.
f ∈ Borel_measurable a ⇔
f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a
My previous idea actually doesn't work. The problem is that, not only ∞ +
-∞, but also the other three cases (-∞ + ∞, ∞ - ∞, -∞ - -∞) will also
involve when you actually try to prove that proposition, and these four
cases have in total 3^4 possible value combinations, none leads to any
inconsistency.
--Chun
On Mon, Jul 27, 2020 at 5:51 PM Manuel Eberl <ebe...@in.tum.de> wrote:
> 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
>
--
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
