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
Cmd instead 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
! This file was ported from Lean 3 source module logic.equiv.list
! leanprover-community/mathlib commit d11893b411025250c8e61ff2f12ccbd7ee35ab15
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Vector.Basic
import Mathlib.Logic.Denumerable
/-!
# Equivalences involving `List`-like types
This file defines some additional constructive equivalences using `Encodable` and the pairing
function on `ℕ`.
-/
open Nat List
namespace Encodable
variable { α : Type _ : Type (?u.12538+1)}
section List
variable [ Encodable α ]
/-- Explicit encoding function for `List α` -/
def encodeList : List α → ℕ
| [] => 0
| a :: l => succ ( pair ( encode a ) ( encodeList l ))
#align encodable.encode_list Encodable.encodeList
/-- Explicit decoding function for `List α` -/
def decodeList : ℕ → Option ( List α )
| 0 => some []
| succ v =>
match unpair v , unpair_right_le : ∀ (n : ℕ ), (unpair n ≤ n v with
| ( v₁ , v₂ ), h =>
have : v₂ < succ v := lt_succ_of_le : ∀ {n m : ℕ }, n ≤ m n < succ m h
(· :: ·) <$> decode (α := α ) v₁ <*> decodeList v₂
#align encodable.decode_list Encodable.decodeList
/-- If `α` is encodable, then so is `List α`. This uses the `pair` and `unpair` functions from
`Data.Nat.Pairing`. -/
instance _root_.List.encodable : Encodable ( List α ) :=
⟨ encodeList , decodeList , fun l => by
induction' l with a l IH <;> simp [ encodeList , decodeList , unpair_pair , encodek , *] ⟩
#align list.encodable List.encodable
instance _root_.List.countable { α : Type _ } [ Countable α ] : Countable ( List α ) := by
haveI := Encodable.ofCountable α
infer_instance
#align list.countable List.countable
@[ simp ]
theorem encode_list_nil : encode (@ nil α ) = 0 :=
rfl : ∀ {α : Sort ?u.9332} {a : α }, a = a
#align encodable.encode_list_nil Encodable.encode_list_nil
@[ simp ]
theorem encode_list_cons ( a : α ) ( l : List α ) :
encode ( a :: l ) = succ ( pair ( encode a ) ( encode l )) :=
rfl : ∀ {α : Sort ?u.9438} {a : α }, a = a
#align encodable.encode_list_cons Encodable.encode_list_cons
@[ simp ]
theorem decode_list_zero : decode (α := List α ) 0 = some [] :=
show decodeList 0 = some [] by rw [ decodeList ]
#align encodable.decode_list_zero Encodable.decode_list_zero
@[ simp , nolint unusedHavesSuffices ] -- Porting note: false positive
theorem decode_list_succ ( v : ℕ ) :
decode (α := List α ) ( succ v ) =
(· :: ·) <$> decode (α := α ) v . unpair . 1 : {α : Type ?u.9820} → {β : Type ?u.9819} → α × β α <*> decode (α := List α ) v . unpair . 2 : {α : Type ?u.9841} → {β : Type ?u.9840} → α × β β :=
show decodeList ( succ v ) = _ by
cases' e : unpair v with v₁ v₂
simp [ decodeList , e ] ; rfl
#align encodable.decode_list_succ Encodable.decode_list_succ
theorem length_le_encode : ∀ l : List α , length l ≤ encode l
| [] => Nat.zero_le : ∀ (n : ℕ ), 0 ≤ n _
| _ :: l => succ_le_succ <| ( length_le_encode l ). trans : ∀ {α : Type ?u.12637} [inst : Preorder α a b c : α }, a ≤ b b ≤ c a ≤ c trans ( right_le_pair : ∀ (a b : ℕ ), b ≤ pair a b _ _ )
#align encodable.length_le_encode Encodable.length_le_encode
end List
section Finset
variable [ Encodable : Type ?u.13761 → Type ?u.13761 α ]
private def enle : α → α → Prop :=
encode ⁻¹'o (· ≤ ·)
private theorem enle.isLinearOrder : IsLinearOrder α enle :=
( RelEmbedding.preimage : {α : Type ?u.13004} → {β : Type ?u.13003} → (f : α ↪ β (s : β → β → Prop ↑f ⁻¹'o s ↪r s ⟨ encode , encode_injective ⟩ (· ≤ ·) ). isLinearOrder
private def decidable_enle : (a b : α ) → Decidable (Encodable.enle a b decidable_enle ( a b : α ) : Decidable ( enle a b ) := by
unfold enle Order.Preimage : {α : Sort u_1} → {β : Sort u_2} → (α → β (β → β → Prop α → α → Prop
infer_instance
attribute [ local instance ] enle.isLinearOrder decidable_enle
/-- Explicit encoding function for `Multiset α` -/
def encodeMultiset ( s : Multiset α ) : ℕ :=
encode ( s . sort enle )
#align encodable.encode_multiset Encodable.encodeMultiset
/-- Explicit decoding function for `Multiset α` -/
def decodeMultiset ( n : ℕ ) : Option ( Multiset α ) :=
( (↑) : List α → Multiset α ) <$> decode (α := List α ) n
#align encodable.decode_multiset Encodable.decodeMultiset
/-- If `α` is encodable, then so is `Multiset α`. -/
instance _root_.Multiset.encodable : Encodable : Type ?u.13992 → Type ?u.13992 ( Multiset α ) :=
⟨ encodeMultiset , decodeMultiset , fun s => by simp [ encodeMultiset , decodeMultiset , encodek ] ⟩
#align multiset.encodable Multiset.encodable
/-- If `α` is countable, then so is `Multiset α`. -/
instance _root_.Multiset.countable { α : Type _ : Type (?u.14780+1)} [ Countable α ] : Countable ( Multiset α ) :=
Quotient.countable
#align multiset.countable Multiset.countable
end Finset
/-- A listable type with decidable equality is encodable. -/
def encodableOfList [ DecidableEq : Sort ?u.14845 → Sort (max1?u.14845) α ] ( l : List α ) ( H : ∀ x , x ∈ l ) : Encodable : Type ?u.14893 → Type ?u.14893 α :=
⟨ fun a => indexOf : {α : Type ?u.14911} → [inst : BEq α α → List α ℕ a l , l . get? , fun _ => indexOf_get? ( H _ )⟩
#align encodable.encodable_of_list Encodable.encodableOfList
/-- A finite type is encodable. Because the encoding is not unique, we wrap it in `Trunc` to
preserve computability. -/
def _root_.Fintype.truncEncodable ( α : Type _ : Type (?u.15217+1)) [ DecidableEq : Sort ?u.15220 → Sort (max1?u.15220) α ] [ Fintype α ] : Trunc ( Encodable : Type ?u.15233 → Type ?u.15233 α ) :=
@ Quot.recOnSubsingleton' _ _ : ?m.15247 → ?m.15247 → Prop ( fun s : Multiset α => (∀ x : α , x ∈ s ) → Trunc ( Encodable : Type ?u.15291 → Type ?u.15291 α )) _
Finset.univ . 1 ( fun l H => Trunc.mk <| encodableOfList l H ) Finset.mem_univ : ∀ {α : Type ?u.15550} [inst : Fintype α x : α ), x ∈ Finset.univ
#align fintype.trunc_encodable Fintype.truncEncodable
/-- A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with `local attribute [instance] Fintype.toEncodable`. -/
noncomputable def _root_.Fintype.toEncodable ( α : Type _ : Type (?u.15748+1)) [ Fintype α ] : Encodable : Type ?u.15754 → Type ?u.15754 α := by
classical exact ( Fintype.truncEncodable α ). out
#align fintype.to_encodable Fintype.toEncodable
/-- If `α` is encodable, then so is `Vector α n`. -/
instance _root_.Vector.encodable [ Encodable : Type ?u.15974 → Type ?u.15974 α ] { n } : Encodable : Type ?u.15980 → Type ?u.15980 ( Vector α n ) :=
Subtype.encodable
#align vector.encodable Vector.encodable
/-- If `α` is countable, then so is `Vector α n`. -/
instance _root_.Vector.countable [ Countable α ] { n } : Countable ( Vector α n ) :=
Subtype.countable
#align vector.countable Vector.countable
/-- If `α` is encodable, then so is `Fin n → α`. -/
instance finArrow [ Encodable : Type ?u.16380 → Type ?u.16380 α ] { n } : Encodable : Type ?u.16386 → Type ?u.16386 ( Fin n → α ) :=
ofEquiv _ ( Equiv.vectorEquivFin : (α : Type ?u.16421) → (n : ℕ ) → Vector α n ≃ (Fin n α _ _ ). symm : {α : Sort ?u.16425} → {β : Sort ?u.16424} → α ≃ β β ≃ α symm
#align encodable.fin_arrow Encodable.finArrow
instance finPi ( n ) ( π : Fin n → Type _ : Type (?u.16515+1)) [∀ i , Encodable : Type ?u.16522 → Type ?u.16522 ( π i )] : Encodable : Type ?u.16526 → Type ?u.16526 (∀ i , π i ) :=
ofEquiv _ ( Equiv.piEquivSubtypeSigma : (ι : Type ?u.16568) → (π : ι → Type ?u.16567((i : ι ) → π i ) ≃ { f // ∀ (i : ι ), (f i = i } ( Fin n ) π )
#align encodable.fin_pi Encodable.finPi
/-- If `α` is encodable, then so is `Finset α`. -/
instance _root_.Finset.encodable [ Encodable : Type ?u.16946 → Type ?u.16946 α ] : Encodable : Type ?u.16949 → Type ?u.16949 ( Finset α ) :=
haveI := decidableEqOfEncodable α
ofEquiv { s : Multiset α // s . Nodup }
⟨ fun ⟨ a , b ⟩ => ⟨ a , b ⟩, fun ⟨ a , b ⟩ => ⟨ a , b ⟩, fun ⟨_, _⟩ => rfl : ∀ {α : Sort ?u.17257} {a : α }, a = a , fun ⟨_, _⟩ => rfl : ∀ {α : Sort ?u.17403} {a : α }, a = a ⟩
#align finset.encodable Finset.encodable
/-- If `α` is countable, then so is `Finset α`. -/
instance _root_.Finset.countable [ Countable α ] : Countable ( Finset α ) :=
Finset.val_injective . countable
#align finset.countable Finset.countable
-- TODO: Unify with `fintypePi` and find a better name
/-- When `α` is finite and `β` is encodable, `α → β` is encodable too. Because the encoding is not
unique, we wrap it in `Trunc` to preserve computability. -/
def fintypeArrow ( α : Type _ : Type (?u.17910+1)) ( β : Type _ : Type (?u.17913+1)) [ DecidableEq : Sort ?u.17916 → Sort (max1?u.17916) α ] [ Fintype α ] [ Encodable : Type ?u.17928 → Type ?u.17928 β ] :
Trunc ( Encodable : Type ?u.17932 → Type ?u.17932 ( α → β )) :=
( Fintype.truncEquivFin α ). map fun f =>
Encodable.ofEquiv ( Fin ( Fintype.card α ) → β ) <| Equiv.arrowCongr : {α₁ : Sort ?u.18017} →
{β₁ : Sort ?u.18016} → {α₂ : Sort ?u.18015} → {β₂ : Sort ?u.18014} → α₁ ≃ α₂ β₁ ≃ β₂ (α₁ → β₁ ≃ (α₂ → β₂ f ( Equiv.refl : (α : Sort ?u.18028) → α ≃ α _ )
#align encodable.fintype_arrow Encodable.fintypeArrow
/-- When `α` is finite and all `π a` are encodable, `Π a, π a` is encodable too. Because the
encoding is not unique, we wrap it in `Trunc` to preserve computability. -/
def fintypePi ( α : Type _ : Type (?u.18192+1)) ( π : α → Type _ : Type (?u.18197+1)) [ DecidableEq : Sort ?u.18200 → Sort (max1?u.18200) α ] [ Fintype α ] [∀ a , Encodable : Type ?u.18216 → Type ?u.18216 ( π a )] :
Trunc ( Encodable : Type ?u.18221 → Type ?u.18221 (∀ a , π a )) :=
( Fintype.truncEncodable α ). bind fun a =>
(@ fintypeArrow α (Σ a , π a ) _ _ (@ Sigma.encodable _ _ : ?m.18310 → Type ?u.18308 a _)). bind fun f =>
Trunc.mk <|
@ Encodable.ofEquiv _ _ (@ Subtype.encodable _ _ f _)
( Equiv.piEquivSubtypeSigma : (ι : Type ?u.18792) → (π : ι → Type ?u.18791((i : ι ) → π i ) ≃ { f // ∀ (i : ι ), (f i = i } α π )
#align encodable.fintype_pi Encodable.fintypePi
/-- The elements of a `Fintype` as a sorted list. -/
def sortedUniv ( α ) [ Fintype α ] [ Encodable : Type ?u.19409 → Type ?u.19409 α ] : List α :=
Finset.univ . sort ( Encodable.encode' α ⁻¹'o (· ≤ ·) )
#align encodable.sorted_univ Encodable.sortedUniv
@[ simp ]
theorem mem_sortedUniv { α } [ Fintype α ] [ Encodable : Type ?u.27416 → Type ?u.27416 α ] ( x : α ) : x ∈ sortedUniv α :=
( Finset.mem_sort _ : ?m.27470 → ?m.27470 → Prop ). 2 : ∀ {a b : Prop }, (a ↔ b b → a ( Finset.mem_univ : ∀ {α : Type ?u.27792} [inst : Fintype α x : α ), x ∈ Finset.univ _ )
#align encodable.mem_sorted_univ Encodable.mem_sortedUniv
@[ simp ]
theorem length_sortedUniv ( α ) [ Fintype α ] [ Encodable : Type ?u.28050 → Type ?u.28050 α ] : ( sortedUniv α ). length = Fintype.card α :=
Finset.length_sort _ : ?m.28079 → ?m.28079 → Prop
#align encodable.length_sorted_univ Encodable.length_sortedUniv
@[ simp ]
theorem sortedUniv_nodup ( α ) [ Fintype α ] [ Encodable : Type ?u.28602 → Type ?u.28602 α ] : ( sortedUniv α ). Nodup :=
Finset.sort_nodup _ : ?m.28630 → ?m.28630 → Prop _
#align encodable.sorted_univ_nodup Encodable.sortedUniv_nodup
@[ simp ]
theorem sortedUniv_toFinset ( α ) [ Fintype α ] [ Encodable : Type ?u.29154 → Type ?u.29154 α ] [ DecidableEq : Sort ?u.29157 → Sort (max1?u.29157) α ] :
( sortedUniv α ). toFinset = Finset.univ :=
Finset.sort_toFinset _ : ?m.29313 → ?m.29313 → Prop _
#align encodable.sorted_univ_to_finset Encodable.sortedUniv_toFinset
/-- An encodable `Fintype` is equivalent to the same size `Fin`. -/
def fintypeEquivFin { α } [ Fintype α ] [ Encodable : Type ?u.29972 → Type ?u.29972 α ] : α ≃ Fin ( Fintype.card α ) :=
haveI : DecidableEq : Sort ?u.29988 → Sort (max1?u.29988) α := Encodable.decidableEqOfEncodable _
-- Porting note: used the `trans` tactic
(( sortedUniv_nodup α ). getEquivOfForallMemList _ mem_sortedUniv ). symm : {α : Sort ?u.30150} → {β : Sort ?u.30149} → α ≃ β β ≃ α symm . trans : {α : Sort ?u.30157} → {β : Sort ?u.30156} → {γ : Sort ?u.30155} → α ≃ β β ≃ γ α ≃ γ trans <|
Equiv.cast : {α β : Sort ?u.30168} → α = β α ≃ β ( congr_arg : ∀ {α : Sort ?u.30174} {β : Sort ?u.30173} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂ _ ( length_sortedUniv α ))
#align encodable.fintype_equiv_fin Encodable.fintypeEquivFin
/-- If `α` and `β` are encodable and `α` is a fintype, then `α → β` is encodable as well. -/
instance fintypeArrowOfEncodable { α β : Type _ : Type (?u.30245+1)} [ Encodable : Type ?u.30248 → Type ?u.30248 α ] [ Fintype α ] [ Encodable : Type ?u.30254 → Type ?u.30254 β ] :
Encodable : Type ?u.30257 → Type ?u.30257 ( α → β ) :=
ofEquiv ( Fin ( Fintype.card α ) → β ) <| Equiv.arrowCongr : {α₁ : Sort ?u.30286} →
{β₁ : Sort ?u.30285} → {α₂ : Sort ?u.30284} → {β₂ : Sort ?u.30283} → α₁ ≃ α₂ β₁ ≃ β₂ (α₁ → β₁ ≃ (α₂ → β₂ fintypeEquivFin ( Equiv.refl : (α : Sort ?u.30356) → α ≃ α _ )
#align encodable.fintype_arrow_of_encodable Encodable.fintypeArrowOfEncodable
end Encodable
namespace Denumerable
variable { α : Type _ : Type (?u.38622+1)} { β : Type _ : Type (?u.43348+1)} [ Denumerable : Type ?u.62387 → Type ?u.62387 α ] [ Denumerable : Type ?u.43767 → Type ?u.43767 β ]
open Encodable
section List
@[ nolint unusedHavesSuffices ] -- Porting note: false positive
theorem denumerable_list_aux : ∀ n : ℕ , ∃ a ∈ @ decodeList α _ n , encodeList a = n
| 0 => by rw [ decodeList ] ; exact ⟨ _ , rfl : ∀ {α : Sort ?u.30756} {a : α }, a = a , rfl : ∀ {α : Sort ?u.30764} {a : α }, a = a ⟩
| succ v => by
cases' e : unpair v with v₁ v₂
have h := unpair_right_le : ∀ (n : ℕ ), (unpair n ≤ n v
rw [ e ] at h
rcases have : v₂ < succ v := lt_succ_of_le : ∀ {n m : ℕ }, n ≤ m n < succ m h
denumerable_list_aux v₂ with
⟨ a , h₁ , h₂ ⟩
rw [ Option.mem_def ] at h₁
use ofNat α v₁ :: a
simp [ decodeList , e , h₂ , h₁ , encodeList , pair_unpair' e ]
#align denumerable.denumerable_list_aux Denumerable.denumerable_list_aux
/-- If `α` is denumerable, then so is `List α`. -/
instance denumerableList : Denumerable : Type ?u.38634 → Type ?u.38634 ( List α ) :=
⟨ denumerable_list_aux ⟩
#align denumerable.denumerable_list Denumerable.denumerableList
@[ simp ]
theorem list_ofNat_zero : ofNat ( List α ) 0 = [] := by rw [ ← @ encode_list_nil α , ofNat_encode ]
#align denumerable.list_of_nat_zero Denumerable.list_ofNat_zero
@[ simp , nolint unusedHavesSuffices ] -- Porting note: false positive
theorem list_ofNat_succ ( v : ℕ ) :
ofNat ( List α ) ( succ v ) = ofNat α v . unpair . 1 : {α : Type ?u.39115} → {β : Type ?u.39114} → α × β α :: ofNat ( List α ) v . unpair . 2 : {α : Type ?u.39125} → {β : Type ?u.39124} → α × β β :=
ofNat_of_decode <|
show decodeList ( succ v ) = _ by
cases' e : unpair v with v₁ v₂
simp [ decodeList , e ]
rw [ show decodeList v₂ = decode (α := List α ) v₂ from rfl : ∀ {α : Sort ?u.43232} {a : α }, a = a , decode_eq_ofNat , Option.seq_some ,
Option.some.injEq : ∀ {α : Type ?u.43278} (val val_1 : α ), (some val = some val_1 = (val = val_1 ]
#align denumerable.list_of_nat_succ Denumerable.list_ofNat_succ
end List
section Multiset
/-- Outputs the list of differences of the input list, that is
`lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]` -/
def lower : List ℕ → ℕ → List ℕ
| [], _ => []
| m :: l , n => ( m - n ) :: lower l m
#align denumerable.lower Denumerable.lower
/-- Outputs the list of partial sums of the input list, that is
`raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]` -/
def raise : List ℕ → ℕ → List ℕ
| [], _ => []
| m :: l , n => ( m + n ) :: raise l ( m + n )
#align denumerable.raise Denumerable.raise
theorem lower_raise : ∀ l n , lower ( raise l n ) n = l
| [], n => rfl : ∀ {α : Sort ?u.44225} {a : α }, a = a
| m :: l , n => by rw [ raise , lower , add_tsub_cancel_right , lower_raise l ]
#align denumerable.lower_raise Denumerable.lower_raise
theorem raise_lower : ∀ { l n }, List.Sorted (· ≤ ·) ( n :: l ) → raise ( lower l n ) n = l
| [], n , _ => rfl : ∀ {α : Sort ?u.45558} {a : α }, a = a
| m :: l , n , h => by
have : n ≤ m := List.rel_of_sorted_cons : ∀ {α : Type ?u.45755} {r : α → α → Prop a : α } {l : List α Sorted r (a :: l ∀ (b : α ), b ∈ l r a b h _ ( l . mem_cons_self : ∀ {α : Type ?u.45783} (a : α ) (l : List α a ∈ a :: l _ )
simp [ raise , lower , tsub_add_cancel_of_le this , raise_lower h . of_cons ]
#align denumerable.raise_lower Denumerable.raise_lower
theorem raise_chain : ∀ l n , List.Chain (· ≤ ·) n ( raise l n )
| [], _ => List.Chain.nil : ∀ {α : Type ?u.47080} {R : α → α → Prop a : α }, Chain R a []
| _ :: _, _ => List.Chain.cons : ∀ {α : Type ?u.47131} {R : α → α → Prop a b : α } {l : List α R a b Chain R b l Chain R a (b :: l ( Nat.le_add_left : ∀ (n m : ℕ ), n ≤ m + n _ _ ) ( raise_chain _ _ )
#align denumerable.raise_chain Denumerable.raise_chain : ∀ (l : List ℕ n : ℕ ), Chain (fun x x_1 => x ≤ x_1 ) n (raise l n
/-- `raise l n` is an non-decreasing sequence. -/
theorem raise_sorted : ∀ l n , List.Sorted (· ≤ ·) ( raise l n )
| [], _ => List.sorted_nil : ∀ {α : Type ?u.47435} {r : α → α → Prop Sorted r []
| _ :: _, _ => List.chain_iff_pairwise . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( raise_chain _ _ )
#align denumerable.raise_sorted Denumerable.raise_sorted : ∀ (l : List ℕ n : ℕ ), Sorted (fun x x_1 => x ≤ x_1 ) (raise l n
/-- If `α` is denumerable, then so is `Multiset α`. Warning: this is *not* the same encoding as used
in `Multiset.encodable`. -/
instance multiset : Denumerable : Type ?u.47775 → Type ?u.47775 ( Multiset α ) :=
mk'
⟨ fun s : Multiset α => encode <| lower (( s . map encode ). sort (· ≤ ·) ) 0 ,
fun n =>
Multiset.map ( ofNat α ) ( raise ( ofNat ( List ℕ ) n ) 0 ),
fun s => by
have :=
raise_lower ( List.sorted_cons . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ fun n _ => Nat.zero_le : ∀ (n : ℕ ), 0 ≤ n n , ( s . map encode ). sort_sorted _ : ?m.48509 → ?m.48509 → Prop ⟩)
simp [- Multiset.coe_map , this ] ,
fun n => by
simp [- Multiset.coe_map , List.mergeSort_eq_self _ : ?m.51745 → ?m.51745 → Prop ( raise_sorted _ _ ), lower_raise ] ⟩
#align denumerable.multiset Denumerable.multiset
end Multiset
section Finset
/-- Outputs the list of differences minus one of the input list, that is
`lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...]`. -/
def lower' : List ℕ → ℕ → List ℕ
| [], _ => []
| m :: l , n => ( m - n ) :: lower' l ( m + 1 )
#align denumerable.lower' Denumerable.lower'
/-- Outputs the list of partial sums plus one of the input list, that is
`raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]`. Adding one each
time ensures the elements are distinct. -/
def raise' : List ℕ → ℕ → List ℕ
| [], _ => []
| m :: l , n => ( m + n ) :: raise' l ( m + n + 1 )
#align denumerable.raise' Denumerable.raise'
theorem lower_raise' : ∀ l n , lower' ( raise' l n ) n = l
| [], n => rfl : ∀ {α : Sort ?u.56261} {a : α }, a = a
| m :: l , n => by simp [ raise' , lower' , add_tsub_cancel_right , lower_raise' ]
#align denumerable.lower_raise' Denumerable.lower_raise'
theorem raise_lower' : ∀ { l n }, (∀ m ∈ l , n ≤ m ) → List.Sorted (· < ·) l → raise' ( lower' l n ) n = l
| [], n , _, _ => rfl : ∀ {α : Sort ?u.58733} {a : α }, a = a
| m :: l , n , h₁ : ∀ (m_1 : ℕ ), m_1 ∈ m :: l n ≤ m_1 h₁ , h₂ => by
have : n ≤ m := h₁ : ∀ (m_1 : ℕ ), m_1 ∈ m :: l n ≤ m_1 h₁ _ ( l . mem_cons_self : ∀ {α : Type ?u.59134} (a : α ) (l : List α a ∈ a :: l _ )
simp [ raise' , lower' , tsub_add_cancel_of_le this ,
raise_lower' ( List.rel_of_sorted_cons : ∀ {α : Type ?u.59540} {r : α → α → Prop a : α } {l : List α Sorted r (a :: l ∀ (b : α ), b ∈ l r a b h₂ : ∀ a ∈ l , m < a ) h₂ . of_cons ]
#align denumerable.raise_lower' Denumerable.raise_lower'
theorem raise'_chain : ∀ ( l ) { m n }, m < n → List.Chain (· < ·) m ( raise' l n )
| [], _, _, _ => List.Chain.nil : ∀ {α : Type ?u.60685} {R : α → α → Prop a : α }, Chain R a []
| _ :: _, _, _, h =>
List.Chain.cons : ∀ {α : Type ?u.60758} {R : α → α → Prop a b : α } {l : List α R a b Chain R b l Chain R a (b :: l ( lt_of_lt_of_le : ∀ {α : Type ?u.60771} [inst : Preorder α a b c : α }, a < b b ≤ c a < c h ( Nat.le_add_left : ∀ (n m : ℕ ), n ≤ m + n _ _ )) ( raise'_chain _ ( lt_succ_self : ∀ (n : ℕ ), n < succ n _ ))
#align denumerable.raise'_chain Denumerable.raise'_chain : ∀ (l : List ℕ m n : ℕ }, m < n Chain (fun x x_1 => x < x_1 ) m (raise' l n
/-- `raise' l n` is a strictly increasing sequence. -/
theorem raise'_sorted : ∀ l n , List.Sorted (· < ·) ( raise' l n )
| [], _ => List.sorted_nil : ∀ {α : Type ?u.61285} {r : α → α → Prop Sorted r []
| _ :: _, _ => List.chain_iff_pairwise . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( raise'_chain _ ( lt_succ_self : ∀ (n : ℕ ), n < succ n _ ))
#align denumerable.raise'_sorted Denumerable.raise'_sorted
/-- Makes `raise' l n` into a finset. Elements are distinct thanks to `raise'_sorted`. -/
def raise'Finset ( l : List ℕ ) ( n : ℕ ) : Finset ℕ :=
⟨ raise' l n , ( raise'_sorted _ _ ). imp (@ ne_of_lt : ∀ {α : Type ?u.61765} [inst : Preorder α a b : α }, a < b a ≠ b _ _)⟩
#align denumerable.raise'_finset Denumerable.raise'Finset
/-- If `α` is denumerable, then so is `Finset α`. Warning: this is *not* the same encoding as used
in `Finset.encodable`. -/
instance finset : Denumerable : Type ?u.62393 → Type ?u.62393 ( Finset α ) :=
mk'
⟨ fun s : Finset α => encode <| lower' (( s . map ( eqv α ). toEmbedding : {α : Sort ?u.62459} → {β : Sort ?u.62458} → α ≃ β α ↪ β toEmbedding ). sort (· ≤ ·) ) 0 , fun n =>
Finset.map ( eqv α ). symm : {α : Sort ?u.62811} → {β : Sort ?u.62810} → α ≃ β β ≃ α symm . toEmbedding : {α : Sort ?u.62815} → {β : Sort ?u.62814} → α ≃ β α ↪ β toEmbedding ( raise'Finset ( ofNat ( List ℕ ) n ) 0 ), fun s =>
Finset.eq_of_veq : ∀ {α : Type ?u.62844} {s t : Finset α s .val= t .vals = t <| by
simp [- Multiset.coe_map , raise'Finset ,
raise_lower' ( fun n _ => Nat.zero_le : ∀ (n : ℕ ), 0 ≤ n n ) ( Finset.sort_sorted_lt _ )] ,
fun n => by
simp [- Multiset.coe_map , Finset.map , raise'Finset , Finset.sort ,
List.mergeSort_eq_self (· ≤ ·) (( raise'_sorted _ _ ). imp (@ le_of_lt : ∀ {α : Type ?u.65128} [inst : Preorder α a b : α }, a < b a ≤ b _ _)), lower_raise' ] ⟩
#align denumerable.finset Denumerable.finset
end Finset
end Denumerable
namespace Equiv
/-- The type lists on unit is canonically equivalent to the natural numbers. -/
def listUnitEquiv : List Unit ≃ ℕ where
toFun := List.length : {α : Type ?u.67879} → List α ℕ
invFun n := List.replicate : {α : Type ?u.67888} → ℕ → α → List α n ()
left_inv u := List.length_injective ( by simp )
right_inv n := List.length_replicate n ()
#align equiv.list_unit_equiv Equiv.listUnitEquiv
/-- `List ℕ` is equivalent to `ℕ`. -/
def listNatEquivNat : List ℕ ≃ ℕ :=
Denumerable.eqv _
#align equiv.list_nat_equiv_nat Equiv.listNatEquivNat
/-- If `α` is equivalent to `ℕ`, then `List α` is equivalent to `α`. -/
def listEquivSelfOfEquivNat : {α : Type u_1} → α ≃ ℕ List α ≃ α listEquivSelfOfEquivNat { α : Type _ : Type (?u.68320+1)} ( e : α ≃ ℕ ) : List α ≃ α :=
calc
List α ≃ List ℕ := listEquivOfEquiv e
_ ≃ ℕ := listNatEquivNat
_ ≃ α := e . symm : {α : Sort ?u.68419} → {β : Sort ?u.68418} → α ≃ β β ≃ α
#align equiv.list_equiv_self_of_equiv_nat Equiv.listEquivSelfOfEquivNat : {α : Type u_1} → α ≃ ℕ List α ≃ α
end Equiv