Miscellaneous #
This is currently not very sorted. PRs welcome!
A product space α × β
is equivalent to the space Π i : Fin 2, γ i
, where
γ = Fin.cons α (Fin.cons β finZeroElim)
. See also piFinTwoEquiv
and
finTwoArrowEquiv
.
Equations
Instances For
@[simp]
theorem
prodEquivPiFinTwo_apply
(α β : Type u)
:
⇑(prodEquivPiFinTwo α β) = fun (p : Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1) =>
Fin.cons p.1 (Fin.cons p.2 finZeroElim)
@[simp]
theorem
prodEquivPiFinTwo_symm_apply
(α β : Type u)
:
⇑(prodEquivPiFinTwo α β).symm = fun (f : (i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) => (f 0, f 1)
The space of functions Fin 2 → α
is equivalent to α × α
. See also piFinTwoEquiv
and
prodEquivPiFinTwo
.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
The equiv version of Fin.predAbove_zero
.
@[simp]
@[simp]
An embedding e : Fin (n+1) ↪ ι
corresponds to an embedding f : Fin n ↪ ι
(corresponding
the last n
coordinates of e
) together with a value not taken by f
(corresponding to e 0
).
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
The equivalence induced by a ↦ (a / n, a % n)
for nonzero n
.
See Int.ediv_emod_unique
for a similar propositional statement.
Equations
Instances For
@[simp]