> Il giorno 18 set 2018, alle ore 11:15, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > 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.
*does NOT require that (f 0 = EMPTY). > > —Chun > >> Il giorno 18 set 2018, alle ore 10:36, Thomas Tuerk <tho...@tuerk-brechen.de >> <mailto: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 <mailto: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
