Monad

📁 Source: Mathlib/Data/Set/Finite/Monad.lean

Statistics

Metric	Count
Definitions fintypeBind, fintypeBind', fintypePure, fintypeSeq, fintypeSeq'	5
Theorems finite_pure, finite_seq, bind, seq, seq'	5
Total	10

Finite.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_pure 📖	mathematical	—	Set.Finite Set Set.instAlternative	—	Set.toFinite Finite.of_fintype
finite_seq 📖	mathematical	—	Finite Set.Elem Set.seq	—	Set.seq_def finite_biUnion' finite_image

Set

Definitions

Name	Category	Theorems
fintypeBind 📖	CompOp	—
fintypeBind' 📖	CompOp	—
fintypePure 📖	CompOp	—
fintypeSeq 📖	CompOp	—
fintypeSeq' 📖	CompOp	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind 📖	mathematical	Set.Finite	Set Set.monad	—	biUnion
seq 📖	mathematical	—	Set.Finite Set.seq	—	image2
seq' 📖	mathematical	—	Set.Finite Set Set.instAlternative	—	seq

---

← Back to Index