Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kenny Lau, Scott Morrison

! This file was ported from Lean 3 source module data.list.fin_range
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.OfFn
import Mathlib.Data.List.Perm

/-!
# Lists of elements of `Fin n`

This file develops some results on `finRange n`.
-/


universe u

namespace List

variable {
α: Type u
α
:
Type u: Type (u+1)
Type u
} @[simp] theorem
map_coe_finRange: ∀ (n : ℕ), map Fin.val (finRange n) = range n
map_coe_finRange
(n :
ℕ: Type
ℕ
) : ((
finRange: (n : ℕ) → List (Fin n)
finRange
n) :
List: Type ?u.10 → Type ?u.10
List
(
Fin: ℕ → Type
Fin
n)).
map: {α : Type ?u.13} → {β : Type ?u.12} → (α → β) → List α → List β
map
(
Fin.val: {n : ℕ} → Fin n → ℕ
Fin.val
) =
List.range: ℕ → List ℕ
List.range
n :=

Goals accomplished! 🐙
α: Type u

n: ℕ


map Fin.val (finRange n) = range n
α: Type u

n: ℕ


map Fin.val (finRange n) = range n
α: Type u

n: ℕ


map Fin.val (pmap Fin.mk (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)) = range n
α: Type u

n: ℕ


map Fin.val (finRange n) = range n
α: Type u

n: ℕ


pmap (fun a h => a) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n) = range n
α: Type u

n: ℕ


map Fin.val (finRange n) = range n
α: Type u

n: ℕ


map (fun a => a) (range n) = range n
α: Type u

n: ℕ


map (fun a => a) (range n) = range n
α: Type u

n: ℕ


map Fin.val (finRange n) = range n

Goals accomplished! 🐙
#align list.map_coe_fin_range
List.map_coe_finRange: ∀ (n : ℕ), map Fin.val (finRange n) = range n
List.map_coe_finRange
theorem
finRange_succ_eq_map: ∀ (n : ℕ), finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
finRange_succ_eq_map
(n :
ℕ: Type
ℕ
) :
finRange: (n : ℕ) → List (Fin n)
finRange
n.
succ: ℕ → ℕ
succ
=
0: ?m.498
0
:: (
finRange: (n : ℕ) → List (Fin n)
finRange
n).
map: {α : Type ?u.508} → {β : Type ?u.507} → (α → β) → List α → List β
map
Fin.succ: {n : ℕ} → Fin n → Fin (Nat.succ n)
Fin.succ
:=

Goals accomplished! 🐙
α: Type u

n: ℕ


finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = ↑0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
range (Nat.succ n) = ↑0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
0 :: map Nat.succ (range n) = ↑0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
0 :: map Nat.succ (range n) = 0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
0 :: map Nat.succ (map Fin.val (finRange n)) = 0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map Fin.val (map Fin.succ (finRange n))
α: Type u

n: ℕ


a
map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α: Type u

n: ℕ


a
0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
α: Type u

n: ℕ


a
0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
α: Type u

n: ℕ


finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)

Goals accomplished! 🐙
#align list.fin_range_succ_eq_map
List.finRange_succ_eq_map: ∀ (n : ℕ), finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
List.finRange_succ_eq_map
-- Porting note : `map_nth_le` moved to `List.finRange_map_get` in Data.List.Range theorem
ofFn_eq_pmap: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
ofFn_eq_pmap
{
α: ?m.851
α
n} {
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.854
n
→
α: ?m.851
α
} :
ofFn: {α : Type ?u.862} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
=
pmap: {α : Type ?u.870} → {β : Type ?u.869} → {p : α → Prop} → ((a : α) → p a → β) → (l : List α) → (∀ (a : α), a ∈ l → p a) → List β
pmap
(fun
i: ?m.875
i
hi: ?m.878
hi
=>
f: Fin n → α
f
⟨
i: ?m.875
i
,
hi: ?m.878
hi
⟩) (
range: ℕ → List ℕ
range
n: ?m.854
n
) fun
_: ?m.892
_
=>
mem_range: ∀ {m n : ℕ}, m ∈ range n ↔ m < n
mem_range
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
:=

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


length (ofFn f) = length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

i: ℕ

hi1: i < length (ofFn f)

hi2: i < length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))


get (ofFn f) { val := i, isLt := hi1 } = get (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))) { val := i, isLt := hi2 }

Goals accomplished! 🐙

Goals accomplished! 🐙
#align list.of_fn_eq_pmap
List.ofFn_eq_pmap: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
List.ofFn_eq_pmap
theorem
ofFn_id: ∀ (n : ℕ), ofFn id = finRange n
ofFn_id
(
n: ?m.2312
n
) :
ofFn: {α : Type ?u.2316} → {n : ℕ} → (Fin n → α) → List α
ofFn
id: {α : Sort ?u.2319} → α → α
id
=
finRange: (n : ℕ) → List (Fin n)
finRange
n: ?m.2312
n
:=
ofFn_eq_pmap: ∀ {α : Type ?u.2352} {n : ℕ} {f : Fin n → α}, ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
ofFn_eq_pmap
#align list.of_fn_id
List.ofFn_id: ∀ (n : ℕ), ofFn id = finRange n
List.ofFn_id
theorem
ofFn_eq_map: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, ofFn f = map f (finRange n)
ofFn_eq_map
{
α: Type u_1
α
n: ?m.2420
n
} {
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.2420
n
→
α: ?m.2417
α
} :
ofFn: {α : Type ?u.2428} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
= (
finRange: (n : ℕ) → List (Fin n)
finRange
n: ?m.2420
n
).
map: {α : Type ?u.2436} → {β : Type ?u.2435} → (α → β) → List α → List β
map
f: Fin n → α
f
:=

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map f (finRange n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map f (finRange n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map f (ofFn id)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map f (finRange n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = ofFn (f ∘ id)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = map f (finRange n)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


ofFn f = ofFn f

Goals accomplished! 🐙
#align list.of_fn_eq_map
List.ofFn_eq_map: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, ofFn f = map f (finRange n)
List.ofFn_eq_map
theorem
nodup_ofFn_ofInjective: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, Function.Injective f → Nodup (ofFn f)
nodup_ofFn_ofInjective
{
α: ?m.2523
α
n: ?m.2526
n
} {
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.2526
n
→
α: ?m.2523
α
} (hf :
Function.Injective: {α : Sort ?u.2534} → {β : Sort ?u.2533} → (α → β) → Prop
Function.Injective
f: Fin n → α
f
) :
Nodup: {α : Type ?u.2542} → List α → Prop
Nodup
(
ofFn: {α : Type ?u.2544} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
) :=

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

hf: Function.Injective f


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

hf: Function.Injective f


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

hf: Function.Injective f


Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n))
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

hf: Function.Injective f


Nodup (pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n))
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

hf: Function.Injective f



Goals accomplished! 🐙
#align list.nodup_of_fn_of_injective
List.nodup_ofFn_ofInjective: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, Function.Injective f → Nodup (ofFn f)
List.nodup_ofFn_ofInjective
theorem
nodup_ofFn: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, Nodup (ofFn f) ↔ Function.Injective f
nodup_ofFn
{
α: Type u_1
α
n} {
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n: ?m.2681
n
→
α: ?m.2678
α
} :
Nodup: {α : Type ?u.2688} → List α → Prop
Nodup
(
ofFn: {α : Type ?u.2690} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
) ↔
Function.Injective: {α : Sort ?u.2700} → {β : Sort ?u.2699} → (α → β) → Prop
Function.Injective
f: Fin n → α
f
:=

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


refine'_1
Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


refine'_1
Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


refine'_1
Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

a✝: Nodup (ofFn Fin.elim0)


refine'_1
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


refine'_1
Nodup (ofFn Fin.elim0) → Function.Injective Fin.elim0

Goals accomplished! 🐙
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α


α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (Fin.cons x₀ xs 0 :: ofFn fun i => Fin.cons x₀ xs (Fin.succ i))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (Fin.cons x₀ xs 0 :: ofFn fun i => xs i)


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: (¬Fin.cons x₀ xs 0 ∈ ofFn fun i => xs i) ∧ Nodup (ofFn fun i => xs i)


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: (¬x₀ ∈ ofFn fun i => xs i) ∧ Nodup (ofFn fun i => xs i)


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: Nodup (ofFn (Fin.cons x₀ xs))


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: (¬x₀ ∈ Set.range fun i => xs i) ∧ Nodup (ofFn fun i => xs i)


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs

h: (¬x₀ ∈ Set.range fun i => xs i) ∧ Nodup (ofFn fun i => xs i)


refine'_2
α✝: Type u

α: Type u_1

n: ℕ

f: Fin n → α

n✝: ℕ

x₀: α

xs: Fin n✝ → α

ih: Nodup (ofFn xs) → Function.Injective xs


refine'_2
Nodup (ofFn (Fin.cons x₀ xs)) → Function.Injective (Fin.cons x₀ xs)

Goals accomplished! 🐙
#align list.nodup_of_fn
List.nodup_ofFn: ∀ {α : Type u_1} {n : ℕ} {f : Fin n → α}, Nodup (ofFn f) ↔ Function.Injective f
List.nodup_ofFn
end List open List theorem
Equiv.Perm.map_finRange_perm: ∀ {n : ℕ} (σ : Perm (Fin n)), map (↑σ) (finRange n) ~ finRange n
Equiv.Perm.map_finRange_perm
{n :
ℕ: Type
ℕ
} (
σ: Perm (Fin n)
σ
:
Equiv.Perm: Sort ?u.3610 → Sort (max1?u.3610)
Equiv.Perm
(
Fin: ℕ → Type
Fin
n)) :
map: {α : Type ?u.3616} → {β : Type ?u.3615} → (α → β) → List α → List β
map
σ: Perm (Fin n)
σ
(
finRange: (n : ℕ) → List (Fin n)
finRange
n) ~
finRange: (n : ℕ) → List (Fin n)
finRange
n :=

Goals accomplished! 🐙
n: ℕ

σ: Perm (Fin n)


map (↑σ) (finRange n) ~ finRange n
n: ℕ

σ: Perm (Fin n)


map (↑σ) (finRange n) ~ finRange n
n: ℕ

σ: Perm (Fin n)


∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
n: ℕ

σ: Perm (Fin n)


∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
n: ℕ

σ: Perm (Fin n)


map (↑σ) (finRange n) ~ finRange n

Goals accomplished! 🐙
#align equiv.perm.map_fin_range_perm
Equiv.Perm.map_finRange_perm: ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)), map (↑σ) (finRange n) ~ finRange n
Equiv.Perm.map_finRange_perm
/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to the list obtained from `f`. -/ theorem
Equiv.Perm.ofFn_comp_perm: ∀ {n : ℕ} {α : Type u} (σ : Perm (Fin n)) (f : Fin n → α), ofFn (f ∘ ↑σ) ~ ofFn f
Equiv.Perm.ofFn_comp_perm
{n :
ℕ: Type
ℕ
} {
α: Type u
α
:
Type u: Type (u+1)
Type u
} (
σ: Perm (Fin n)
σ
:
Equiv.Perm: Sort ?u.8670 → Sort (max1?u.8670)
Equiv.Perm
(
Fin: ℕ → Type
Fin
n)) (
f: Fin n → α
f
:
Fin: ℕ → Type
Fin
n →
α: Type u
α
) :
ofFn: {α : Type ?u.8679} → {n : ℕ} → (Fin n → α) → List α
ofFn
(
f: Fin n → α
f
∘
σ: Perm (Fin n)
σ
) ~
ofFn: {α : Type ?u.8781} → {n : ℕ} → (Fin n → α) → List α
ofFn
f: Fin n → α
f
:=

Goals accomplished! 🐙
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


ofFn (f ∘ ↑σ) ~ ofFn f
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


ofFn (f ∘ ↑σ) ~ ofFn f
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


map (f ∘ ↑σ) (finRange n) ~ ofFn f
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


ofFn (f ∘ ↑σ) ~ ofFn f
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


map (f ∘ ↑σ) (finRange n) ~ map f (finRange n)
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


ofFn (f ∘ ↑σ) ~ ofFn f
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


map f (map (↑σ) (finRange n)) ~ map f (finRange n)
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


map f (map (↑σ) (finRange n)) ~ map f (finRange n)
n: ℕ

α: Type u

σ: Perm (Fin n)

f: Fin n → α


ofFn (f ∘ ↑σ) ~ ofFn f

Goals accomplished! 🐙
#align equiv.perm.of_fn_comp_perm
Equiv.Perm.ofFn_comp_perm: ∀ {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α), ofFn (f ∘ ↑σ) ~ ofFn f
Equiv.Perm.ofFn_comp_perm