Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2022 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen, Alex J. Best

! This file was ported from Lean 3 source module data.finsupp.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 Mathlib.Data.Finsupp.Defs
import Mathlib.Data.Fintype.Basic

/-!

# Finiteness and infiniteness of `Finsupp`

Some lemmas on the combination of `Finsupp`, `Fintype` and `Infinite`.

-/


noncomputable instance 
Finsupp.fintype: {ι : Type u_1} → {π : Type u_2} → [inst : DecidableEq ι] → [inst : Zero π] → [inst_1 : Fintype ι] → [inst_2 : Fintype π] → Fintype (ι →₀ π)
Finsupp.fintype
{
ι: Sort ?u.2
ι
π: Sort ?u.5
π
:
Sort _: Type ?u.2
Sort
Sort _: Type ?u.2
_
} [
DecidableEq: Sort ?u.8 → Sort (max1?u.8)
DecidableEq
ι: Sort ?u.2
ι
] [
Zero: Type ?u.17 → Type ?u.17
Zero
π: Sort ?u.5
π
] [
Fintype: Type ?u.20 → Type ?u.20
Fintype
ι: Sort ?u.2
ι
] [
Fintype: Type ?u.23 → Type ?u.23
Fintype
π: Sort ?u.5
π
] :
Fintype: Type ?u.26 → Type ?u.26
Fintype
(
ι: Sort ?u.2
ι
→₀
π: Sort ?u.5
π
) :=
Fintype.ofEquiv: {β : Type ?u.54} → (α : Type ?u.53) → [inst : Fintype α] → α βFintype β
Fintype.ofEquiv
_: Type ?u.53
_
Finsupp.equivFunOnFinite: {α : Type ?u.135} → {M : Type ?u.134} → [inst : Zero M] → [inst_1 : Finite α] → (α →₀ M) (αM)
Finsupp.equivFunOnFinite
.
symm: {α : Sort ?u.244} → {β : Sort ?u.243} → α ββ α
symm
#align finsupp.fintype
Finsupp.fintype: {ι : Type u_1} → {π : Type u_2} → [inst : DecidableEq ι] → [inst : Zero π] → [inst_1 : Fintype ι] → [inst_2 : Fintype π] → Fintype (ι →₀ π)
Finsupp.fintype
instance
Finsupp.infinite_of_left: ∀ {ι : Type u_1} {π : Type u_2} [inst : Nontrivial π] [inst : Zero π] [inst_1 : Infinite ι], Infinite (ι →₀ π)
Finsupp.infinite_of_left
{
ι: Sort ?u.425
ι
π: Type ?u.431
π
:
Sort _: Type ?u.428
Sort
Sort _: Type ?u.428
_
} [
Nontrivial: Type ?u.431 → Prop
Nontrivial
π: Sort ?u.428
π
] [
Zero: Type ?u.434 → Type ?u.434
Zero
π: Sort ?u.428
π
] [
Infinite: Sort ?u.437 → Prop
Infinite
ι: Sort ?u.425
ι
] :
Infinite: Sort ?u.440 → Prop
Infinite
(
ι: Sort ?u.425
ι
→₀
π: Sort ?u.428
π
) := let ⟨_,
hm: w✝ 0
hm
⟩ :=
exists_ne: ∀ {α : Type ?u.465} [inst : Nontrivial α] (x : α), y, y x
exists_ne
(
0: ?m.470
0
:
π: Type ?u.431
π
)
Infinite.of_injective: ∀ {α : Sort ?u.546} {β : Sort ?u.547} [inst : Infinite β] (f : βα), Function.Injective fInfinite α
Infinite.of_injective
_: ?m.549?m.548
_
<|
Finsupp.single_left_injective: ∀ {α : Type ?u.582} {M : Type ?u.581} [inst : Zero M] {b : M}, b 0Function.Injective fun a => single a b
Finsupp.single_left_injective
hm: w✝ 0
hm
#align finsupp.infinite_of_left
Finsupp.infinite_of_left: ∀ {ι : Type u_1} {π : Type u_2} [inst : Nontrivial π] [inst : Zero π] [inst_1 : Infinite ι], Infinite (ι →₀ π)
Finsupp.infinite_of_left
instance
Finsupp.infinite_of_right: ∀ {ι : Type u_1} {π : Type u_2} [inst : Infinite π] [inst : Zero π] [inst_1 : Nonempty ι], Infinite (ι →₀ π)
Finsupp.infinite_of_right
{
ι: Sort ?u.764
ι
π: Sort ?u.767
π
:
Sort _: Type ?u.767
Sort
Sort _: Type ?u.767
_
} [
Infinite: Sort ?u.770 → Prop
Infinite
π: Sort ?u.767
π
] [
Zero: Type ?u.773 → Type ?u.773
Zero
π: Sort ?u.767
π
] [
Nonempty: Sort ?u.776 → Prop
Nonempty
ι: Sort ?u.764
ι
] :
Infinite: Sort ?u.779 → Prop
Infinite
(
ι: Sort ?u.764
ι
→₀
π: Sort ?u.767
π
) :=
Infinite.of_injective: ∀ {α : Sort ?u.803} {β : Sort ?u.804} [inst : Infinite β] (f : βα), Function.Injective fInfinite α
Infinite.of_injective
(fun
i: ?m.840
i
=>
Finsupp.single: {α : Type ?u.843} → {M : Type ?u.842} → [inst : Zero M] → αMα →₀ M
Finsupp.single
(
Classical.arbitrary: (α : Sort ?u.888) → [h : Nonempty α] → α
Classical.arbitrary
ι: Type ?u.781
ι
)
i: ?m.840
i
) (
Finsupp.single_injective: ∀ {α : Type ?u.918} {M : Type ?u.917} [inst : Zero M] (a : α), Function.Injective (single a)
Finsupp.single_injective
(
Classical.arbitrary: (α : Sort ?u.922) → [h : Nonempty α] → α
Classical.arbitrary
ι: Type ?u.781
ι
)) #align finsupp.infinite_of_right
Finsupp.infinite_of_right: ∀ {ι : Type u_1} {π : Type u_2} [inst : Infinite π] [inst : Zero π] [inst_1 : Nonempty ι], Infinite (ι →₀ π)
Finsupp.infinite_of_right