> Il giorno 18 set 2018, alle ore 11:15, Chun Tian (binghe)
> 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.
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 ∈ st
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
no… by drawing pictures and think it more, this statement is still not true, if
the set is general (of type ‘a -> bool).
please forget the whole question. I must have assumed something wrong in
earlier places. thanks all the same.
—Chun
> Il giorno 18 set 2018, alle ore 10:25, Chun Tian (bingh
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
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[]
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)
> ha scritto:
>
> Hi,
>
> I ran into the following goal in the proof of a big theorem:
>
> ∃x. a ⊆ f x
>
