Functor

📁 Source: Mathlib/Data/Set/Functor.lean

Statistics

Metric	Count
Definitions instAlternative, monad, SetM, run, instAlternativeMonadSetM	5
Theorems bind_def, coe_eq_image_val, coe_subset, eq_univ_of_coe_eq, eq_univ_of_image_val_eq, failure_def, fmap_eq_image, image2_def, image_coe_eq_restrict_image, image_image_val_eq_restrict_image, image_val_subset, instCommApplicative, instLawfulAlternative, instLawfulMonad, mem_coe_of_mem, mem_image_val_of_mem, mem_of_mem_coe, mem_of_mem_image_val, orElse_def, pure_def, seqLeft_def, seqRight_def, seq_eq_set_seq, instLawfulAlternativeSetM, instLawfulMonadSetM	25
Total	30

Set

Definitions

Name	Category	Theorems
instAlternative 📖	CompOp	14 math math: Filter.mem_traverse_iff, pure_def, instCommApplicative, image2_def, orElse_def, instLawfulAlternative, Finite.Set.finite_pure, Filter.mem_traverse, seq_eq_set_seq, seqLeft_def, seqRight_def, Finite.seq', failure_def, List.mem_traverse
monad 📖	CompOp	7 math math: image_coe_eq_restrict_image, instLawfulMonad, coe_eq_image_val, mem_coe_of_mem, coe_subset, bind_def, Finite.bind

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind_def 📖	mathematical	—	Set monad iUnion instMembership	—	—
coe_eq_image_val 📖	mathematical	—	Set Elem instCoeTCElem monad image instMembership	—	ext iUnion_coe_set iUnion_congr_Prop
coe_subset 📖	mathematical	—	Set instHasSubset monad Elem instMembership	—	—
eq_univ_of_coe_eq 📖	mathematical	Set monad Elem instMembership	univ	—	eq_univ_of_forall mem_of_mem_coe
eq_univ_of_image_val_eq 📖	mathematical	image Set instMembership	univ Elem	—	eq_univ_of_forall mem_of_mem_image_val
failure_def 📖	mathematical	—	Set instAlternative instEmptyCollection	—	—
fmap_eq_image 📖	mathematical	—	Set instFunctor image	—	—
image2_def 📖	mathematical	—	image2 Set instAlternative instFunctor	—	ext
image_coe_eq_restrict_image 📖	mathematical	—	image Set monad Elem instMembership restrict	—	ext coe_subset mem_of_mem_coe mem_coe_of_mem
image_image_val_eq_restrict_image 📖	mathematical	—	image Set instMembership Elem restrict	—	ext image_congr
image_val_subset 📖	mathematical	—	Set instHasSubset image instMembership	—	Subtype.coe_image_subset
instCommApplicative 📖	mathematical	—	CommApplicative Set instAlternative	—	instLawfulAlternative prod_image_seq_comm
instLawfulAlternative 📖	mathematical	—	Set instAlternative	—	instLawfulFunctor image_congr singleton_seq image_singleton seq_singleton seq_seq image_empty image2_empty_left union_empty empty_union union_assoc image_union
instLawfulMonad 📖	mathematical	—	Set monad	—	CommApplicative.toLawfulApplicative instCommApplicative image_eq_iUnion seq_def biUnion_singleton biUnion_iUnion
mem_coe_of_mem 📖	mathematical	Set instMembership Elem	monad	—	—
mem_image_val_of_mem 📖	mathematical	Set instMembership Elem	image	—	—
mem_of_mem_coe 📖	mathematical	Set instMembership monad Elem	coe_subset	—	coe_subset
mem_of_mem_image_val 📖	mathematical	Set instMembership image	Elem image_val_subset	—	image_val_subset
orElse_def 📖	mathematical	—	Set instAlternative instUnion	—	—
pure_def 📖	mathematical	—	Set instAlternative instSingletonSet	—	—
seqLeft_def 📖	mathematical	—	Set instAlternative setOf instMembership Nonempty	—	—
seqRight_def 📖	mathematical	—	Set instAlternative setOf Nonempty instMembership	—	—
seq_eq_set_seq 📖	mathematical	—	Set instAlternative seq	—	—

SetM

Definitions

Name	Category	Theorems
run 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
SetM 📖	CompOp	2 math math: instLawfulAlternativeSetM, instLawfulMonadSetM
instAlternativeMonadSetM 📖	CompOp	2 math math: instLawfulAlternativeSetM, instLawfulMonadSetM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternativeSetM 📖	mathematical	—	SetM instAlternativeMonadSetM	—	Set.instLawfulAlternative
instLawfulMonadSetM 📖	mathematical	—	SetM instAlternativeMonadSetM	—	Set.instLawfulMonad

---

← Back to Index