Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-11 11:44 c062d9ea

View on Github →

feat(*): more bundled versions of (fin 2 → α) ≃ (α × α) (#10214) Also ensure that the inverse function uses vector notation when possible.

Estimated changes

modified def fin_two_arrow_equiv
added def homeomorph.{u}