@[simp]
@[simp]
theorem
piFinTwoEquiv_symm_apply
(α : Fin 2 → Type u)
:
↑(piFinTwoEquiv α).symm = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)
Π 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
.
Instances For
@[simp]
theorem
prodEquivPiFinTwo_symm_apply
(α : Type u)
(β : Type u)
:
↑(prodEquivPiFinTwo α β).symm = fun f => (f 0, f 1)
@[simp]
theorem
prodEquivPiFinTwo_apply
(α : Type u)
(β : Type u)
:
↑(prodEquivPiFinTwo α β) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)
A product space α × β
is equivalent to the space Π i : Fin 2, γ i
, where
γ = Fin.cons α (Fin.cons β finZeroElim)
. See also piFinTwoEquiv
and
finTwoArrowEquiv
.
Instances For
@[simp]
theorem
finTwoArrowEquiv_apply
(α : Type u_1)
:
↑(finTwoArrowEquiv α) = (piFinTwoEquiv fun x => α).toFun
@[simp]
theorem
finTwoArrowEquiv_symm_apply
(α : Type u_1)
:
↑(finTwoArrowEquiv α).symm = fun x => ![x.fst, x.snd]
The space of functions Fin 2 → α
is equivalent to α × α
. See also piFinTwoEquiv
and
prodEquivPiFinTwo
.
Instances For
The space of functions Fin 2 → α
is order equivalent to α × α
. See also
OrderIso.piFinTwoIso
.
Instances For
@[simp]
theorem
finSuccEquiv'_succAbove
{n : ℕ}
(i : Fin (n + 1))
(j : Fin n)
:
↑(finSuccEquiv' i) (Fin.succAbove i j) = some j
theorem
finSuccEquiv'_below
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : Fin.castSucc m < i)
:
↑(finSuccEquiv' i) (Fin.castSucc m) = some m
theorem
finSuccEquiv'_above
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : i ≤ Fin.castSucc m)
:
↑(finSuccEquiv' i) (Fin.succ m) = some m
@[simp]
@[simp]
theorem
finSuccEquiv'_symm_some
{n : ℕ}
(i : Fin (n + 1))
(j : Fin n)
:
↑(finSuccEquiv' i).symm (some j) = Fin.succAbove i j
theorem
finSuccEquiv'_symm_some_below
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : Fin.castSucc m < i)
:
↑(finSuccEquiv' i).symm (some m) = Fin.castSucc m
theorem
finSuccEquiv'_symm_some_above
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : i ≤ Fin.castSucc m)
:
↑(finSuccEquiv' i).symm (some m) = Fin.succ m
theorem
finSuccEquiv'_symm_coe_below
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : Fin.castSucc m < i)
:
↑(finSuccEquiv' i).symm (some m) = Fin.castSucc m
theorem
finSuccEquiv'_symm_coe_above
{n : ℕ}
{i : Fin (n + 1)}
{m : Fin n}
(h : i ≤ Fin.castSucc m)
:
↑(finSuccEquiv' i).symm (some m) = Fin.succ m
@[simp]
@[simp]
The equiv version of Fin.predAbove_zero
.
theorem
finSuccEquiv'_last_apply_castSucc
{n : ℕ}
(i : Fin n)
:
↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some i
theorem
finSuccEquiv'_last_apply
{n : ℕ}
{i : Fin (n + 1)}
(h : i ≠ Fin.last n)
:
↑(finSuccEquiv' (Fin.last n)) i = some (Fin.castLT i (_ : ↑i < n))
theorem
finSuccEquiv'_ne_last_apply
{n : ℕ}
{i : Fin (n + 1)}
{j : Fin (n + 1)}
(hi : i ≠ Fin.last n)
(hj : j ≠ i)
:
↑(finSuccEquiv' i) j = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) j)
theorem
finSuccAboveEquiv_apply
{n : ℕ}
(p : Fin (n + 1))
(i : Fin n)
:
↑(finSuccAboveEquiv p) i = { val := Fin.succAbove p i, property := (_ : Fin.succAbove p i ≠ p) }
theorem
finSuccAboveEquiv_symm_apply_last
{n : ℕ}
(x : { x // x ≠ Fin.last n })
:
↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x = Fin.castLT ↑x (_ : ↑↑x < n)
theorem
finSuccAboveEquiv_symm_apply_ne_last
{n : ℕ}
{p : Fin (n + 1)}
(h : p ≠ Fin.last n)
(x : { x // x ≠ p })
:
↑(OrderIso.symm (finSuccAboveEquiv p)) x = Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x
@[simp]
@[simp]
theorem
finSuccEquivLast_symm_some
{n : ℕ}
(i : Fin n)
:
↑finSuccEquivLast.symm (some i) = Fin.castSucc i
@[simp]
theorem
Equiv.piFinSuccAboveEquiv_apply
{n : ℕ}
(α : Fin (n + 1) → Type u)
(i : Fin (n + 1))
:
↑(Equiv.piFinSuccAboveEquiv α i) = fun f => (f i, fun j => f (Fin.succAbove i j))
@[simp]
theorem
Equiv.piFinSuccAboveEquiv_symm_apply
{n : ℕ}
(α : Fin (n + 1) → Type u)
(i : Fin (n + 1))
:
↑(Equiv.piFinSuccAboveEquiv α i).symm = fun f => Fin.insertNth i f.fst f.snd
@[simp]
theorem
Equiv.piFinSucc_apply
(n : ℕ)
(β : Type u)
:
↑(Equiv.piFinSucc n β) = fun f => (f 0, fun j => f (Fin.succ j))
@[simp]
theorem
Equiv.piFinSucc_symm_apply
(n : ℕ)
(β : Type u)
:
↑(Equiv.piFinSucc n β).symm = fun f => Fin.cons f.fst f.snd
@[simp]
theorem
finSumFinEquiv_apply_left
{m : ℕ}
{n : ℕ}
(i : Fin m)
:
↑finSumFinEquiv (Sum.inl i) = Fin.castAdd n i
@[simp]
theorem
finSumFinEquiv_apply_right
{m : ℕ}
{n : ℕ}
(i : Fin n)
:
↑finSumFinEquiv (Sum.inr i) = Fin.natAdd m i
@[simp]
theorem
finSumFinEquiv_symm_apply_castAdd
{m : ℕ}
{n : ℕ}
(x : Fin m)
:
↑finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x
@[simp]
theorem
finSumFinEquiv_symm_apply_natAdd
{m : ℕ}
{n : ℕ}
(x : Fin n)
:
↑finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x
@[simp]
theorem
finAddFlip_apply_castAdd
{m : ℕ}
(k : Fin m)
(n : ℕ)
:
↑finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
@[simp]
theorem
finAddFlip_apply_natAdd
{n : ℕ}
(k : Fin n)
(m : ℕ)
:
↑finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
@[simp]
theorem
finProdFinEquiv_symm_apply
{m : ℕ}
{n : ℕ}
(x : Fin (m * n))
:
↑finProdFinEquiv.symm x = (Fin.divNat x, Fin.modNat x)
@[simp]
@[simp]
theorem
Int.divModEquiv_apply
(n : ℕ)
[NeZero n]
(a : ℤ)
:
↑(Int.divModEquiv n) a = (a / ↑n, ↑(Int.natMod a ↑n))
The equivalence induced by a ↦ (a / n, a % n)
for nonzero n
.
See Int.ediv_emod_unique
for a similar propositional statement.
Instances For
@[simp]
theorem
Fin.castLEOrderIso_symm_apply
{n : ℕ}
{m : ℕ}
(h : n ≤ m)
(i : { i // ↑i < n })
:
↑(RelIso.symm (Fin.castLEOrderIso h)) i = { val := ↑↑i, isLt := (_ : ↑↑i < n) }
@[simp]
theorem
Fin.castLEOrderIso_apply
{n : ℕ}
{m : ℕ}
(h : n ≤ m)
(i : Fin n)
:
↑(Fin.castLEOrderIso h) i = { val := Fin.castLE h i, property := (_ : ↑i < n) }