Equivalence between Fin 2
and Bool
.
Equations
- finTwoEquiv = { toFun := ![false, true], invFun := fun (b : Bool) => Bool.casesOn b 0 1, left_inv := finTwoEquiv.proof_2, right_inv := finTwoEquiv.proof_3 }
Instances For
Π i : Fin 2, α i
is equivalent to α 0 × α 1
. See also finTwoArrowEquiv
for a
non-dependent version and prodEquivPiFinTwo
for a version with inputs α β : Type u
.
Equations
Instances For
A product space α × β
is equivalent to the space Π i : Fin 2, γ i
, where
γ = Fin.cons α (Fin.cons β finZeroElim)
. See also piFinTwoEquiv
and
finTwoArrowEquiv
.
Equations
- prodEquivPiFinTwo α β = (piFinTwoEquiv (Fin.cons α (Fin.cons β finZeroElim))).symm
Instances For
The space of functions Fin 2 → α
is equivalent to α × α
. See also piFinTwoEquiv
and
prodEquivPiFinTwo
.
Equations
- finTwoArrowEquiv α = let __src := piFinTwoEquiv fun (x : Fin 2) => α; { toFun := __src.toFun, invFun := fun (x : α × α) => ![x.1, x.2], left_inv := ⋯, right_inv := ⋯ }
Instances For
Π i : Fin 2, α i
is order equivalent to α 0 × α 1
. See also OrderIso.finTwoArrowEquiv
for a non-dependent version.
Equations
- OrderIso.piFinTwoIso α = { toEquiv := piFinTwoEquiv α, map_rel_iff' := ⋯ }
Instances For
The space of functions Fin 2 → α
is order equivalent to α × α
. See also
OrderIso.piFinTwoIso
.
Equations
- OrderIso.finTwoArrowIso α = let __src := OrderIso.piFinTwoIso fun (x : Fin 2) => α; { toEquiv := finTwoArrowEquiv α, map_rel_iff' := ⋯ }
Instances For
An equivalence that removes i
and maps it to none
.
This is a version of Fin.predAbove
that produces Option (Fin n)
instead of
mapping both i.cast_succ
and i.succ
to i
.
Equations
- finSuccEquiv' i = { toFun := i.insertNth none some, invFun := fun (x : Option (Fin n)) => x.casesOn' i i.succAbove, left_inv := ⋯, right_inv := ⋯ }
Instances For
The equiv version of Fin.predAbove_zero
.
Fin.succAbove
as an order isomorphism between Fin n
and {x : Fin (n + 1) // x ≠ p}
.
Equations
- finSuccAboveEquiv p = let __src := (Equiv.optionSubtype p) ⟨(finSuccEquiv' p).symm, ⋯⟩; { toEquiv := __src, map_rel_iff' := ⋯ }
Instances For
Order isomorphism between Π j : Fin (n + 1), α j
and
α i × Π j : Fin n, α (Fin.succAbove i j)
.
Equations
- OrderIso.piFinSuccAboveIso α i = { toEquiv := Equiv.piFinSuccAbove α i, map_rel_iff' := ⋯ }
Instances For
Equivalence between Fin (n + 1) → β
and β × (Fin n → β)
.
Equations
- Equiv.piFinSucc n β = Equiv.piFinSuccAbove (fun (x : Fin (n + 1)) => β) 0
Instances For
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
- Equiv.embeddingFinSucc n ι = ((finSuccEquiv n).embeddingCongr (Equiv.refl ι)).trans (Function.Embedding.optionEmbeddingEquiv (Fin n) ι)
Instances For
Equivalence between Fin (n + 1) → β
and β × (Fin n → β)
which separates out the last
element of the tuple.
Equations
- Equiv.piFinCastSucc n β = Equiv.piFinSuccAbove (fun (x : Fin (n + 1)) => β) (Fin.last n)
Instances For
Equivalence between Fin m ⊕ Fin n
and Fin (m + n)
Equations
- finSumFinEquiv = { toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m), invFun := fun (i : Fin (m + n)) => Fin.addCases Sum.inl Sum.inr i, left_inv := ⋯, right_inv := ⋯ }
Instances For
The equivalence induced by a ↦ (a / n, a % n)
for nonzero n
.
This is like finProdFinEquiv.symm
but with m
infinite.
See Nat.div_mod_unique
for a similar propositional statement.
Equations
Instances For
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
Promote a Fin n
into a larger Fin m
, as a subtype where the underlying
values are retained. This is the OrderIso
version of Fin.castLE
.
Equations
- Fin.castLEOrderIso h = { toFun := fun (i : Fin n) => ⟨Fin.castLE h i, ⋯⟩, invFun := fun (i : { i : Fin m // ↑i < n }) => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
Fin 0
is a subsingleton.
Equations
Fin 1
is a subsingleton.