From a1be4136c8fac4d4d1ca43ac64d209e9cbc91e14 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Sun, 29 Jan 2023 15:44:37 -0800 Subject: [PATCH 1/5] feat: port Data.FunLike.Fintype From e987b0ef13fbe31bfc6c3551753ae010402faffe Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Sun, 29 Jan 2023 15:44:37 -0800 Subject: [PATCH 2/5] Initial file copy from mathport --- Mathlib/Data/FunLike/Fintype.lean | 82 +++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) create mode 100644 Mathlib/Data/FunLike/Fintype.lean diff --git a/Mathlib/Data/FunLike/Fintype.lean b/Mathlib/Data/FunLike/Fintype.lean new file mode 100644 index 0000000000000..f656bd83d736b --- /dev/null +++ b/Mathlib/Data/FunLike/Fintype.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2022 Anne Baanen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anne Baanen + +! This file was ported from Lean 3 source module data.fun_like.fintype +! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Data.Finite.Basic +import Mathbin.Data.Fintype.Basic +import Mathbin.Data.FunLike.Basic + +/-! +# Finiteness of `fun_like` types + +We show a type `F` with a `fun_like F α β` is finite if both `α` and `β` are finite. +This corresponds to the following two pairs of declarations: + + * `fun_like.fintype` is a definition stating all `fun_like`s are finite if their domain and + codomain are. + * `fun_like.finite` is a lemma stating all `fun_like`s are finite if their domain and + codomain are. + * `fun_like.fintype'` is a non-dependent version of `fun_like.fintype` and + * `fun_like.finite` is a non-dependent version of `fun_like.finite`, because dependent instances + are harder to infer. + +You can use these to produce instances for specific `fun_like` types. +(Although there might be options for `fintype` instances with better definitional behaviour.) +They can't be instances themselves since they can cause loops. +-/ + + +section Type + +variable (F G : Type _) {α γ : Type _} {β : α → Type _} [FunLike F α β] [FunLike G α fun _ => γ] + +/-- All `fun_like`s are finite if their domain and codomain are. + +This is not an instance because specific `fun_like` types might have a better-suited definition. + +See also `fun_like.finite`. +-/ +noncomputable def FunLike.fintype [DecidableEq α] [Fintype α] [∀ i, Fintype (β i)] : Fintype F := + Fintype.ofInjective _ FunLike.coe_injective +#align fun_like.fintype FunLike.fintype + +/-- All `fun_like`s are finite if their domain and codomain are. + +Non-dependent version of `fun_like.fintype` that might be easier to infer. +This is not an instance because specific `fun_like` types might have a better-suited definition. +-/ +noncomputable def FunLike.fintype' [DecidableEq α] [Fintype α] [Fintype γ] : Fintype G := + FunLike.fintype G +#align fun_like.fintype' FunLike.fintype' + +end Type + +section Sort + +variable (F G : Sort _) {α γ : Sort _} {β : α → Sort _} [FunLike F α β] [FunLike G α fun _ => γ] + +/-- All `fun_like`s are finite if their domain and codomain are. + +Can't be an instance because it can cause infinite loops. +-/ +theorem FunLike.finite [Finite α] [∀ i, Finite (β i)] : Finite F := + Finite.of_injective _ FunLike.coe_injective +#align fun_like.finite FunLike.finite + +/-- All `fun_like`s are finite if their domain and codomain are. + +Non-dependent version of `fun_like.finite` that might be easier to infer. +Can't be an instance because it can cause infinite loops. +-/ +theorem FunLike.finite' [Finite α] [Finite γ] : Finite G := + FunLike.finite G +#align fun_like.finite' FunLike.finite' + +end Sort + From bdf5d7962996553bf3cda2a29994b92c5a91f5e3 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Sun, 29 Jan 2023 15:44:38 -0800 Subject: [PATCH 3/5] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Data/FunLike/Fintype.lean | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 9377c64c6d2d6..884e8f8785669 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -329,6 +329,7 @@ import Mathlib.Data.Fintype.Vector import Mathlib.Data.FunLike.Basic import Mathlib.Data.FunLike.Embedding import Mathlib.Data.FunLike.Equiv +import Mathlib.Data.FunLike.Fintype import Mathlib.Data.HashMap import Mathlib.Data.Int.AbsoluteValue import Mathlib.Data.Int.Associated diff --git a/Mathlib/Data/FunLike/Fintype.lean b/Mathlib/Data/FunLike/Fintype.lean index f656bd83d736b..26fcc29ed5c44 100644 --- a/Mathlib/Data/FunLike/Fintype.lean +++ b/Mathlib/Data/FunLike/Fintype.lean @@ -8,9 +8,9 @@ Authors: Anne Baanen ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Data.Finite.Basic -import Mathbin.Data.Fintype.Basic -import Mathbin.Data.FunLike.Basic +import Mathlib.Data.Finite.Basic +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.FunLike.Basic /-! # Finiteness of `fun_like` types From f7110c3e1b3dcde6ac6538d06b3d64a65b5b9852 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Sun, 29 Jan 2023 15:47:22 -0800 Subject: [PATCH 4/5] fix section names --- Mathlib/Data/FunLike/Fintype.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/FunLike/Fintype.lean b/Mathlib/Data/FunLike/Fintype.lean index 26fcc29ed5c44..1a481a7657211 100644 --- a/Mathlib/Data/FunLike/Fintype.lean +++ b/Mathlib/Data/FunLike/Fintype.lean @@ -31,8 +31,8 @@ You can use these to produce instances for specific `fun_like` types. They can't be instances themselves since they can cause loops. -/ - -section Type +-- porting notes: `Type` is a reserved word, switched to `Type'` +section Type' variable (F G : Type _) {α γ : Type _} {β : α → Type _} [FunLike F α β] [FunLike G α fun _ => γ] @@ -55,9 +55,10 @@ noncomputable def FunLike.fintype' [DecidableEq α] [Fintype α] [Fintype γ] : FunLike.fintype G #align fun_like.fintype' FunLike.fintype' -end Type +end Type' -section Sort +-- porting notes: `Sort` is a reserved word, switched to `Sort'` +section Sort' variable (F G : Sort _) {α γ : Sort _} {β : α → Sort _} [FunLike F α β] [FunLike G α fun _ => γ] @@ -78,5 +79,4 @@ theorem FunLike.finite' [Finite α] [Finite γ] : Finite G := FunLike.finite G #align fun_like.finite' FunLike.finite' -end Sort - +end Sort' From d7f32b45e1eccb33fa2926be37bc5c52353439c2 Mon Sep 17 00:00:00 2001 From: Arien Malec Date: Sun, 29 Jan 2023 15:48:06 -0800 Subject: [PATCH 5/5] auto: naming --- Mathlib/Data/FunLike/Fintype.lean | 34 +++++++++++++++---------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/Mathlib/Data/FunLike/Fintype.lean b/Mathlib/Data/FunLike/Fintype.lean index 1a481a7657211..6af0db8c3e9ca 100644 --- a/Mathlib/Data/FunLike/Fintype.lean +++ b/Mathlib/Data/FunLike/Fintype.lean @@ -13,21 +13,21 @@ import Mathlib.Data.Fintype.Basic import Mathlib.Data.FunLike.Basic /-! -# Finiteness of `fun_like` types +# Finiteness of `FunLike` types -We show a type `F` with a `fun_like F α β` is finite if both `α` and `β` are finite. +We show a type `F` with a `FunLike F α β` is finite if both `α` and `β` are finite. This corresponds to the following two pairs of declarations: - * `fun_like.fintype` is a definition stating all `fun_like`s are finite if their domain and + * `FunLike.fintype` is a definition stating all `FunLike`s are finite if their domain and codomain are. - * `fun_like.finite` is a lemma stating all `fun_like`s are finite if their domain and + * `FunLike.finite` is a lemma stating all `FunLike`s are finite if their domain and codomain are. - * `fun_like.fintype'` is a non-dependent version of `fun_like.fintype` and - * `fun_like.finite` is a non-dependent version of `fun_like.finite`, because dependent instances + * `FunLike.fintype'` is a non-dependent version of `FunLike.fintype` and + * `FunLike.finite` is a non-dependent version of `FunLike.finite`, because dependent instances are harder to infer. -You can use these to produce instances for specific `fun_like` types. -(Although there might be options for `fintype` instances with better definitional behaviour.) +You can use these to produce instances for specific `FunLike` types. +(Although there might be options for `Fintype` instances with better definitional behaviour.) They can't be instances themselves since they can cause loops. -/ @@ -36,20 +36,20 @@ section Type' variable (F G : Type _) {α γ : Type _} {β : α → Type _} [FunLike F α β] [FunLike G α fun _ => γ] -/-- All `fun_like`s are finite if their domain and codomain are. +/-- All `FunLike`s are finite if their domain and codomain are. -This is not an instance because specific `fun_like` types might have a better-suited definition. +This is not an instance because specific `FunLike` types might have a better-suited definition. -See also `fun_like.finite`. +See also `FunLike.finite`. -/ noncomputable def FunLike.fintype [DecidableEq α] [Fintype α] [∀ i, Fintype (β i)] : Fintype F := Fintype.ofInjective _ FunLike.coe_injective #align fun_like.fintype FunLike.fintype -/-- All `fun_like`s are finite if their domain and codomain are. +/-- All `FunLike`s are finite if their domain and codomain are. -Non-dependent version of `fun_like.fintype` that might be easier to infer. -This is not an instance because specific `fun_like` types might have a better-suited definition. +Non-dependent version of `FunLike.fintype` that might be easier to infer. +This is not an instance because specific `FunLike` types might have a better-suited definition. -/ noncomputable def FunLike.fintype' [DecidableEq α] [Fintype α] [Fintype γ] : Fintype G := FunLike.fintype G @@ -62,7 +62,7 @@ section Sort' variable (F G : Sort _) {α γ : Sort _} {β : α → Sort _} [FunLike F α β] [FunLike G α fun _ => γ] -/-- All `fun_like`s are finite if their domain and codomain are. +/-- All `FunLike`s are finite if their domain and codomain are. Can't be an instance because it can cause infinite loops. -/ @@ -70,9 +70,9 @@ theorem FunLike.finite [Finite α] [∀ i, Finite (β i)] : Finite F := Finite.of_injective _ FunLike.coe_injective #align fun_like.finite FunLike.finite -/-- All `fun_like`s are finite if their domain and codomain are. +/-- All `FunLike`s are finite if their domain and codomain are. -Non-dependent version of `fun_like.finite` that might be easier to infer. +Non-dependent version of `FunLike.finite` that might be easier to infer. Can't be an instance because it can cause infinite loops. -/ theorem FunLike.finite' [Finite α] [Finite γ] : Finite G :=