Documentation

Mathlib.Data.FunLike.Fintype

Finiteness of FunLike types #

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:

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.

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

All FunLikes are finite if their domain and codomain are.

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

See also FunLike.finite.

Equations
noncomputable def FunLike.fintype' (G : Type u_1) {α : Type u_2} {γ : Type u_3} [inst : FunLike G α fun x => γ] [inst : DecidableEq α] [inst : Fintype α] [inst : Fintype γ] :

All FunLikes are finite if their domain and codomain are.

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.

Equations
theorem FunLike.finite (F : Sort u_3) {α : Sort u_1} {β : αSort u_2} [inst : FunLike F α β] [inst : Finite α] [inst : ∀ (i : α), Finite (β i)] :

All FunLikes 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_3) {α : Sort u_1} {γ : Sort u_2} [inst : FunLike G α fun x => γ] [inst : Finite α] [inst : Finite γ] :

All FunLikes are finite if their domain and codomain are.

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