DFunLike.finite
theorem DFunLike.finite :
∀ (F : Sort u_1) {α : Sort u_3} {β : α → Sort u_5} [inst : DFunLike F α β] [inst : Finite α]
[inst : ∀ (i : α), Finite (β i)], Finite F
This theorem states that all `DFunLike` (dependent function-like) types are finite if their domain and codomain are finite. However, it cannot be an instance because this could cause infinite loops. In other words, for any sort `F`, given that `F` behaves like a dependent function from `α` to `β`, and both `α` and each `β i` (for all `i` in the domain `α`) are finite, then `F` is also finite.
More concisely: If `α` and the codomain of every dependent function-like type `F : α → β_i` have finite sizes, then `F` has a finite size.
|
FunLike.finite
theorem FunLike.finite :
∀ (G : Sort u_2) {α : Sort u_3} {γ : Sort u_4} [inst : FunLike G α γ] [inst : Finite α] [inst : Finite γ],
Finite G
The theorem `FunLike.finite` states that for any sort `G`, and any sorts `α` and `γ`, if `G` has a `FunLike` instance from `α` to `γ`, and if `α` and `γ` are both finite, then `G` is also finite. This is a non-dependent version of `DFunLike.finite` and might be easier to infer. However, it can't be used as an instance because it could cause infinite loops. This theorem essentially tells us about a property of the finiteness of function-like structures in Lean 4.
More concisely: If `G` is a sort with a `FunLike` instance from finite sorts `α` and `γ`, then `G` is finite.
|