IMPS Geometry Library Home Page

Copyright (c) 1990-1994 The MITRE Corporation

Authors: M. Nadel, F. J. Thayer Fábrega

Contents:

Theories

  • geometry-1
  • geometry-2
  • geometry-3
  • geometry-4
  • geometry-5
  • three-place-predicate-theory

    • Translations

  • generic-theory-1-to-geometry
  • iterate->three-place-predicate
  • rel-to-coll

    • Theorems

  • a-singleton-containing-a-particular-element
  • between-implies-collinear-contra
  • cardinality-at-least-2
  • cardinality-at-least-2-lemma
  • cardinality-at-least-3-lemma
  • cardinality-at-most-1-lemma
  • cardinality-of-connecting%lines-bound
  • coll%closed-closed-under-le
  • coll%closed-iff-fixed-under-coll%closure
  • coll%closure-exists
  • coll%closure-of-pair
  • coll-conjunctive-permuter
  • coll-disjunctive-permuter
  • collinear-all-cases
  • collinear-flipper-1-2
  • collinear-flipper-1-3
  • collinear-flipper-2-3
  • collinear-implies-distinct
  • collinear-implies-distinct-lemma
  • connecting%lines-of-finite-sets-are-finite
  • contains-an-element-implies-non-empty
  • definedness-of-le
  • distinctness-2-3
  • empty-segment-lemma
  • emptyset-equals-its-coll%closure
  • emptyset-is-coll%closed
  • existence-right
  • extending
  • extending-collinear-sets
  • f_card_difference
  • finitely-many-on%connecting%line
  • finitely-many-on%connecting%line%through
  • implication-equivalent
  • inequality-2
  • injectivity-of-trace
  • intersection-of-les-with-common-first-point
  • intersection-of-two-les
  • intersection-of-two-lines
  • iota-free-characterization-of-rel%closure
  • iota-free-characterization-of-trace%on%line
  • is-pair-implies-non-empty
  • is-singleton-implies-non-empty
  • is-triple-implies-non-empty
  • le-contains-left-point
  • le-equality-condition
  • le-equals-its-coll%closure
  • le-is-a-line
  • le-is-coll%closed
  • le-is-collinear
  • le-is-symmetric
  • les-are-connecting-lines
  • line-intersects-at-most-two-sides-of-a-triangle-lemma-1
  • lines-are-infinite
  • lines-are-le
  • lines-contain-two-points
  • lines-exist
  • monotonicity-of-coll%closure
  • monotonicity-of-span
  • nesting
  • nesting-2
  • non-collinear
  • non-collinear-2
  • non-collinear-2-other
  • non-collinear-between
  • non-collinear-left
  • non-collinear-right
  • non-equality-1
  • on%connecting%line%through-characterization
  • on%connecting%line-characterization
  • other-extending
  • other-nesting
  • other-point-lemma
  • other-switching
  • pairs-are-collinear
  • rel%closed-iff-fixed-under-span
  • rel%closure-exists
  • sandwich
  • sandwich-lemma
  • segments-are-collinear
  • singleton-equals-its-coll%closure
  • singleton-is-coll%closed
  • singletons-are-collinear
  • span-definedness
  • span-includes-set
  • span-invariance
  • strong-monotonicity-of-iterate
  • switching-all-cases
  • sylvester-lemma-1
  • sylvester-lemma-2
  • sylvester-lemma-3
  • sylvester-lemma-4
  • trace%on%line-undefined-case
  • triple-switching
  • two-points-determine-a-line
  • union%of%iterates-closed-under-span
  • union%of%iterates-includes-s
  • union%of%iterates-is-rel%closure
  • universe-equals-its-coll%closure
  • universe-is-coll%closed
  • weak-pasch-ordered
  • weak-pasch-ordered-lemma
  • weak-pasch-other

    • Defined Constants

  • coll
  • coll%closed
  • coll%closure
  • coll_set
  • connecting%lines
  • connecting%lines%through
  • le
  • line
  • on%connecting%line
  • on%connecting%line%through
  • rel%closed
  • rel%closure
  • seg
  • span
  • trace%on%line
  • union%of%iterates

    • Recursive Constants

    There are none.

    Compound Macetes

  • le-contains-point
    • _______________________________________________________

    This page designed and maintained by F. Javier Thayer Fábrega
    jt@bariloche.mitretek.org