Documentation Verification Report

Set

📁 Source: Mathlib/Logic/Small/Set.lean

Statistics

MetricCount
Definitions0
Theoremssmall_biInter, small_biInter', small_biUnion, small_diff, small_empty, small_iInter, small_iInter', small_iUnion, small_image, small_image2, small_insert, small_inter_of_left, small_inter_of_right, small_pair, small_powerset, small_range, small_sInter, small_sInter', small_sUnion, small_sep, small_setPi, small_setProd, small_single, small_subset, small_union, small_univ, small_univ_iff
27
Total27

(root)

Theorems

NameKindAssumesProvesValidatesDepends On
small_biInter 📖mathematicalSet
Set.instMembership		Small
Set.Elem
Set.iInter		—small_iInter
Set.biInter_eq_iInter
small_biInter' 📖mathematicalSmall
Set.Elem		Set.iInter
Set
Set.instMembership		—small_biInter
Subtype.prop
small_biUnion 📖mathematicalSmall
Set.Elem		Set.iUnion
Set
Set.instMembership		—small_iUnion
Set.biUnion_eq_iUnion
small_diff 📖mathematical—Small
Set.Elem
Set
Set.instSDiff		—small_subset
Set.diff_subset
small_empty 📖mathematical—Small
Set.Elem
Set
Set.instEmptyCollection		—small_subsingleton
IsEmpty.instSubsingleton
Set.instIsEmptyElemEmptyCollection
small_iInter 📖mathematical—Small
Set.Elem
Set.iInter		—small_subset
Set.iInter_subset
small_iInter' 📖mathematicalSmall
Set.Elem		Set.iInter—small_iInter
small_iUnion 📖mathematicalSmall
Set.Elem		Set.iUnion—small_of_surjective
small_sigma
Set.sigmaToiUnion_surjective
small_image 📖mathematical—Small
Set.Elem
Set.image		—small_of_surjective
Set.imageFactorization_surjective
small_image2 📖mathematical—Small
Set.Elem
Set.image2		—Set.image_uncurry_prod
small_image
small_setProd
small_insert 📖mathematical—Small
Set.Elem
Set
Set.instInsert		—small_union
small_subsingleton
Unique.instSubsingleton
Set.insert_eq
small_inter_of_left 📖mathematical—Small
Set.Elem
Set
Set.instInter		—small_subset
Set.inter_subset_left
small_inter_of_right 📖mathematical—Small
Set.Elem
Set
Set.instInter		—small_subset
Set.inter_subset_right
small_pair 📖mathematical—Small
Set.Elem
Set
Set.instInsert
Set.instSingletonSet		—small_insert
small_subsingleton
Unique.instSubsingleton
small_powerset 📖mathematical—Small
Set.Elem
Set
Set.powerset		—small_map
small_set
small_range 📖mathematical—Small
Set.Elem
Set.range		—small_of_surjective
Set.rangeFactorization_surjective
small_sInter 📖mathematicalSet
Set.instMembership		Small
Set.Elem
Set.sInter		—small_iInter
Set.sInter_eq_iInter
small_sInter' 📖mathematicalSmall
Set.Elem
Set
Set.instMembership		Set.sInter—small_sInter
Subtype.prop
small_sUnion 📖mathematicalSmall
Set.Elem
Set
Set.instMembership		Set.sUnion—small_iUnion
Set.sUnion_eq_iUnion
small_sep 📖mathematical—Small
Set.Elem
setOf
Set
Set.instMembership		—small_subset
Set.sep_subset
small_setPi 📖mathematicalSmall
Set.Elem		Set.pi
Set.univ		—small_of_injective
small_Pi
Equiv.injective
small_setProd 📖mathematical—Small
Set.Elem
SProd.sprod
Set
Set.instSProd		—small_of_injective
small_prod
Equiv.injective
small_single 📖mathematical—Small
Set.Elem
Set
Set.instSingletonSet		—small_subsingleton
Unique.instSubsingleton
small_subset 📖mathematicalSet
Set.instHasSubset		Small
Set.Elem		—small_of_injective
Set.inclusion_injective
small_union 📖mathematical—Small
Set.Elem
Set
Set.instUnion		—Subtype.range_val
Set.Sum.elim_range
small_range
small_sum
small_univ 📖mathematical—Small
Set.Elem
Set.univ		—small_univ_iff
small_univ_iff 📖mathematical—Small
Set.Elem
Set.univ		—small_congr

---

← Back to Index