Finiteness of DFunLike types

We show a type F with a DFunLike F α β is finite if both α and β are finite. This corresponds to the following two pairs of declarations:

• DFunLike.fintype is a definition stating all DFunLikes are finite if their domain and codomain are.
• DFunLike.finite is a lemma stating all DFunLikes are finite if their domain and codomain are.
• FunLike.fintype is a non-dependent version of DFunLike.fintype and
• FunLike.finite is a non-dependent version of DFunLike.finite, because dependent instances are harder to infer.

You can use these to produce instances for specific DFunLike types. (Although there might be options for Fintype instances with better definitional behaviour.) They can't be instances themselves since they can cause loops.

noncomputable def DFunLike.fintype (F : Type u_1) {α : Type u_3} {β : α → Type u_5} [DFunLike F α β] [DecidableEq α] [Fintype α] [(i : α) → Fintype (β i)] : Fintype F

All DFunLikes are finite if their domain and codomain are.

This is not an instance because specific DFunLike types might have a better-suited definition.

See also DFunLike.finite.

Equations

• DFunLike.fintype F = Fintype.ofInjective (fun (f : F) => ⇑f) ⋯

noncomputable def FunLike.fintype (G : Type u_2) {α : Type u_3} {γ : Type u_4} [FunLike G α γ] [DecidableEq α] [Fintype α] [Fintype γ] : Fintype G

All FunLikes are finite if their domain and codomain are.

Non-dependent version of DFunLike.fintype that might be easier to infer. This is not an instance because specific FunLike types might have a better-suited definition.

Equations

• FunLike.fintype G = DFunLike.fintype G

theorem DFunLike.finite (F : Sort u_1) {α : Sort u_3} {β : α → Sort u_5} [DFunLike F α β] [Finite α] [∀ (i : α), Finite (β i)] : Finite F

All DFunLikes are finite if their domain and codomain are.

Can't be an instance because it can cause infinite loops.

theorem FunLike.finite (G : Sort u_2) {α : Sort u_3} {γ : Sort u_4} [FunLike G α γ] [Finite α] [Finite γ] : Finite G

All FunLikes are finite if their domain and codomain are.

Non-dependent version of DFunLike.finite that might be easier to infer. Can't be an instance because it can cause infinite loops.

@[instance 100]

instance FunLike.toDecidableEq {F : Type u_1} {α : Type u_2} {β : Type u_3} [DecidableEq β] [Fintype α] [FunLike F α β] : DecidableEq F

Equations

• FunLike.toDecidableEq a b = decidable_of_iff (⇑a = ⇑b) ⋯