Commit 2024-01-07 11:52 de9d093d

View on Github →

feat: add trans assoc type lemmas for (Partial)Equiv and (Partial)Homeomorph (#9506) Let es denote Equivs and fs denote PartialEquivs. Let > denote Equiv.trans, PartialEquiv.trans, Equiv.transPartialEquiv, or PartialEquiv.transEquiv. We want to simplify expressions like e1 > e2 > f3 > f4 > e5 > e6 to (e1 > e2) > (f3 > f4) > (e5 > e6), so that simp lemmas about Equiv.trans and PartialEquiv.trans may apply. This means adding four lemmas:

  1. e1 > e2 > f3 = (e1 > e2) > f3
  2. (e1 > f2) > f3 = e1 > (f2 > f3)
  3. (1) with e and f flipped
  4. (2) with e and f flipped The definitions Equiv.transPartialEquiv and PartialEquiv.transEquiv are moved to later in the document, so that they stay together with these lemmas. The argument order of these two definitions has also been reversed so as to match Equiv.trans and PartialEquiv.trans. The same is done for Homeomorph/PartialHomeomorph.

Estimated changes