mathlib3 documentation

data.fun_like.fintype

Finiteness of fun_like types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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.

source
noncomputable def fun_like.fintype (F : Type u_1) {α : Type u_3} {β : α → Type u_5} [fun_like F α β] [decidable_eq α] [fintype α] [Π (i : α), fintype (β i)] :
fintype F

All fun_likes 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.

Equations
source
noncomputable def fun_like.fintype' (G : Type u_2) {α : Type u_3} {γ : Type u_4} [fun_like G α (λ (_x : α), γ)] [decidable_eq α] [fintype α] [fintype γ] :
fintype G

All fun_likes 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.

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

All fun_likes are finite if their domain and codomain are.

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

source
theorem fun_like.finite' (G : Sort u_2) {α : Sort u_3} {γ : Sort u_4} [fun_like G α (λ (_x : α), γ)] [finite α] [finite γ] :
finite G

All fun_likes 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.