todo.txt

Items which may be doable without a network connection:

* Maybe DRY up CollinearityCollinearity. The lemmas for the various pieces of the
  distributivity in breaking up the 9 cases would reduce duplicative proofs, but
  might be slightly awkward to name.

* Set theory
  - intersection, difference (e.g. eldifi and similar)
  - state A = B ↔ { A } = { B } ? (see sneqr)
  - indexed union or intersection? (if needed for functions)
  - prove Peano axioms from set theory
    - suc11
  - finite induction (e.g. peano5 in set.mm)
  - functions and relations (e.g. cxp and following in set.mm)
    - binary relations.
      - releq (builder for relation predicate)
      (makeRelation a A b B φ) (A, B object; a, b variable; φ formula)
        ≝ {〈a, b〉| a ∈ A ∧ b ∈ B ∧ φ }
        ≝ { z ∈ A × B | ∃ a ∃ b z = 〈 a, b 〉 ∧ φ }
        e.g. (mkrelation a ℕ b ℕ (∃ n ∈ ℕ a + n = b))
        This is a variation of df-opab which restricts the domain and range of the relation. We need this kind of restriction
        because we assume the [[Interface:Axiom of quantifiability]] which means that we can only introduce a notation for
        something which exists (as a set).
      - (relates s (mkrelation a A b B φ) t) ↔ [s / a][t / b]φ  (probably some distinct)
    - domain and range
      - breldm, brelrn
      - (domain (makeRelation a A b B φ)) ⊆ A
      - (range (makeRelation a A b B φ)) ⊆ B
      - (relation { 〈A, B〉 } )
        { 〈A, B〉 } = { A } × { B }
        B ≠ ∅ → domain (A × B) = A (dmxp)
    - functions
      - dffun2 (how to deal with the distinct variables?), funrel
      (lambda x t)
        e.g. (lambda x A 〈x, 1〉)
        ≝ {〈x, result〉| x ∈ A ∧ result = t }
      - [s / x](apply (lambda x A t) s) = t
        this reads oddly, because [/] only applies to formulas, not terms
        (metamath has underlined [/] for terms; do we want that?)
    - cross products
      - (relation A) ↔ ∃ x ∃ y A ⊆ x × y
      - (relation A) ↔ A ⊆ domain A × range A  (right?)
  - recursion theorem (see downloaded wikipedia page, Joedit)
    = frfnom and friends in set.mm
      - e.g. http://us.metamath.org/mpeuni/df-rdg.html

* Needed to derive geometry axioms from reals (page 201 of Givant1999)
  - For CongruenceIdentity
    • 0 ≤ x ∧ 0 ≤ y ∧ x + y = 0 → x = 0 (or some such)
  - For Indivisibility
    • (x - y) · (y - x) ≤ 0
    • antisymmetry
    • (x - y) · (y - x) = 0 → x = y (follows from x · y = 0 → x = 0 or y = 0)

To do with network:

* notation for congruent angles. Convention is ∠ABC ≅ ∠DEF, right?  Then maybe (A B C ∠≅ D E F) for us?