Freek, how does you prove ?! in miz3, that something exists uniquely?
I couldn't find that in your paper or any Mizar dox. Here's a ?
result I proved in (proof below) where I wanted ?!
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar
OrderedCongruentSegments_THM : thm =
|- ! A B C D F.
~(A = C) /\ ~(D = F)
==> Segment A C === Segment D F
==> B IN open (A,C)
==> (? E. E IN open (D,F) /\ Segment A B === Segment D E)
I can live without ?! in this case, but I'm curious how it's done.
--
Best,
Bill
let OrderedCongruentSegments_THM = thm `;
let A B C D F be point;
assume ~(A = C) /\ ~(D = F) [H1];
assume Segment A C === Segment D F [H2];
assume B IN open (A,C) [H3];
thus ? E. E IN open (D,F) /\ Segment A B === Segment D E
proof
~(A = B) /\ ~(B = C) /\ Collinear A C B [ABC] by B1', H3,
CollinearSymmetry_THM;
~(A IN open (B,C)) by ABC, H3, B3', B1';
B IN ray A C DELETE A [BrAC] by H1, ABC, -, IN, Ray_DEF, IN_DELETE;
C IN ray A C DELETE A [CrAC] by H1, EndpointInRay_THM, IN_DELETE;
consider E such that
E IN ray D F DELETE D /\ Segment D E === Segment A B [DE_AB] by ABC,
H1, C1;
~(E = D) /\ Collinear D E F /\ ~(D IN open (F,E)) [ErDF_D] by -, IN,
IN_DELETE, Ray_DEF, B1', CollinearSymmetry_THM;
Segment A B === Segment D E [AB_DE] by ABC, -, DE_AB, C2Symmetric;
~(E = F) [EnotF]
proof
assume E = F;
Segment A B === Segment A C [AB_AC] by -, H1, ABC, H2, DE_AB,
C2Transitive, C2Symmetric;
Segment A C === Segment A C by H1, C2Reflexive;
B = C by H1, BrAC, AB_AC, CrAC, -, C1;
qed by -, ABC;
~(F IN open (E,D))
proof
assume F IN open (E,D);
F IN open (D,E) [DFE] by -, B1';
consider G such that
C IN open (A,G) /\ Segment C G === Segment F E [CG_FE] by EnotF, H1,
C1OppositeRay_THM;
~(A = C) /\ ~(A = G) /\ ~(G = C) /\ Collinear A C G [AnotG] by -, B1';
~(A IN open (G,C)) by -, CG_FE, B3';
G IN ray A C DELETE A [GrayAC] by H1, AnotG, -, IN, Ray_DEF,
IN_DELETE;
Segment A G === Segment D E [AG_DE] by CG_FE, DFE, H2, CG_FE, C3;
B = G [BG] by ErDF_D, H1, BrAC, GrayAC, AB_DE, AG_DE, C1;
B IN open (A,G) by CG_FE, IntervalsAreConvex_THM, H3, SUBSET;
qed by BG, -, B1';
E IN open (D,F) by ErDF_D, H1, EnotF, -, B3';
qed by AB_DE, -`;;
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
