Nuprl Lemma : geo-perp-in_functionality

∀e:BasicGeometry. ∀x:Point.
  ∀[a,b,c,d:Point].
    ∀x':Point
      ∀[a',b',c',d':Point].
        (uiff(ab  ⊥x cd;a'b'  ⊥x' c'd')) supposing (d ≡ d' and c ≡ c' and b ≡ b' and a ≡ a' and x ≡ x')


Proof



Definitions occuring in Statement :  geo-perp-in: ab  ⊥x cd,  basic-geometry: BasicGeometry,  geo-eq: a ≡ b,  geo-point: Point,  uiff: uiff(P;Q),  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x]
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  uiff: uiff(P;Q),  and: P ∧ Q,  geo-perp-in: ab  ⊥x cd,  geo-colinear: Colinear(a;b;c),  not: ¬A,  implies: P ⇒ Q,  false: False,  right-angle: Rabc,  geo-congruent: ab ≅ cd,  prop: ℙ,  subtype_rel: A ⊆r B,  guard: {T},  basic-geometry: BasicGeometry,  rev_implies: P ⇐ Q,  iff: P ⇐⇒ Q
Latex:
\mforall{}e:BasicGeometry.  \mforall{}x:Point.
    \mforall{}[a,b,c,d:Point].
        \mforall{}x':Point
            \mforall{}[a',b',c',d':Point].
                (uiff(ab    \mbot{}x  cd;a'b'    \mbot{}x'  c'd'))  supposing 
                      (d  \mequiv{}  d'  and 
                      c  \mequiv{}  c'  and 
                      b  \mequiv{}  b'  and 
                      a  \mequiv{}  a'  and 
                      x  \mequiv{}  x')


Date html generated: 2020_05_20-AM-09_58_14
Last ObjectModification: 2019_12_26-PM-08_32_52

Theory : euclidean!plane!geometry


Home Index