Hi Thomas, yes, you’re totally right. My original problem cannot be resolved just in scope of set theory. I’m trying to prove the uniqueness of measure:
[UNIQUENESS_OF_MEASURE]
∀sp sts f u v.
sp ∈ sts ∧ subset_class sp sts ∧
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (𝕌(:num) -> sts) ∧
(∀n. f n ⊆ f (SUC n)) ∧ (sp = BIGUNION (IMAGE f 𝕌(:num))) ∧
measure_space (sp,subsets (sigma sp sts),u) ∧
measure_space (sp,subsets (sigma sp sts),v) ∧
(∀n. u (f n) < PosInf) ∧ (∀s. s ∈ sts ⇒ (u s = v s)) ⇒
∀s. s ∈ subsets (sigma sp sts) ⇒ (u s = v s)
And I was approaching a measure (u a) using the sup of an image:
u a = sup (IMAGE (u ∘ (λi. f i ∩ a)) 𝕌(:num))
in which (u :’a set -> extreal) is a measure function, f is the increasing
sequence that I mentioned before. Now I believe the correct way to reduce “sup”
is to use the following non-trivial monotone convergence theorem already in
HOL’s measureTheory:
[MONOTONE_CONVERGENCE]
⊢ ∀m s f.
measure_space m ∧ f ∈ (𝕌(:num) -> measurable_sets m) ∧
(∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 𝕌(:num))) ⇒
(sup (IMAGE (measure m ∘ f) 𝕌(:num)) = measure m s)
Above theorem does require that (f 0 = EMPTY), as I expected. Now I have
confidence to finish the whole proof.
—Chun
> Il giorno 18 set 2018, alle ore 10:36, Thomas Tuerk <tho...@tuerk-brechen.de>
> ha scritto:
>
> Hi Chun,
>
> no, it still does not hold. The problem is that case that "a" might be
> infinite and while there is for every element 'e' of 'a' an 'n' with 'e IN f
> n' you need arbitrary large ones.
>
> A tiny modification of Ramana's counterexample is
>
> f x := count x
> sp := UNIV
> a := { n | even n }
> Cheers
>
> Thomas
>
> On 18.09.2018 10:25, Chun Tian (binghe) wrote:
>> Hi Ramana,
>>
>> thanks for your help. Sorry, I realized that the case “a = sp” can be
>> eliminated from other assumptions, thus I actually have another constraint
>> “a ≠ sp” in my original goals:
>>
>> ∃x. a ⊆ f x
>> ------------------------------------
>> 4. f 0 = ∅
>> 5. ∀i j. i ≤ j ⇒ f i ⊆ f j
>> 6. BIGUNION (IMAGE f 𝕌(:num)) = sp
>> 21. a ≠ sp
>> 23. ∀n. f n ⊆ sp
>> 24. a ⊆ sp
>>
>> in this case your opposite proof doesn’t work any more. Also, I replaced the
>> monotonicity of f into another form, I don’t know which one is easier to
>> use. The assumption "f 0 = ∅” should be optional, I guess.
>>
>> Now this should be a true statement, right?
>>
>> —Chun
>>
>>> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar <ram...@kumar.id.au
>>> <mailto:ram...@kumar.id.au>> ha scritto:
>>>
>>> I think this is false. Here's a proof of the opposite, with the type of f
>>> instantiated to a num set generator:
>>>
>>> val thm = Q.prove(
>>> `¬(
>>> ∀(f:num->num->bool) a sp.
>>> (f 0 = ∅) ∧
>>> (∀n. f n ⊆ f (SUC n)) ∧
>>> (∀n. f n ⊆ sp) ∧
>>> (BIGUNION (IMAGE f 𝕌(:num)) = sp) ∧
>>> (a ⊆ sp) ⇒
>>> ∃x. a ⊆ f x)`,
>>> rw[]
>>> \\ qexists_tac`count`
>>> \\ qexists_tac`UNIV`
>>> \\ rw[SUBSET_DEF, PULL_EXISTS]
>>> >- metis_tac[]
>>> >- (
>>> rw[Once EXTENSION]
>>> \\ qexists_tac`count (SUC x)`
>>> \\ rw[] )
>>> >- (
>>> rw[EXTENSION]
>>> \\ qexists_tac`SUC x`
>>> \\ rw[] ));
>>>
>>>
>>> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) <binghe.l...@gmail.com
>>> <mailto:binghe.l...@gmail.com>> wrote:
>>> sorry, I also have this necessary assumption:
>>>
>>> 5. BIGUNION (IMAGE f 𝕌(:num)) = sp
>>>
>>> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe)
>>> > <binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> ha scritto:
>>> >
>>> > Hi,
>>> >
>>> > I ran into the following goal in the proof of a big theorem:
>>> >
>>> > ∃x. a ⊆ f x
>>> > ------------------------------------
>>> > 3. f 0 = ∅
>>> > 4. ∀n. f n ⊆ f (SUC n)
>>> > 20. ∀n. f n ⊆ sp
>>> > 21. a ⊆ sp
>>> >
>>> > I have an increasing sequence of sets (f n) from empty to the whole space
>>> > (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can
>>> > always choose a big enough index x such that (f x) will contain “a”. But
>>> > how can I make this argument formal?
>>> >
>>> > thanks,
>>> >
>>> > Chun
>>> >
>>>
>>> _______________________________________________
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
>>
>>
>>
>>
>>
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
