Documentation Verification Report

Sigma

📁 Source: Mathlib/Data/Finset/Sigma.lean

Statistics

Metric	Count
Definitions `sigma`, `sigmaLift`	2
Theorems `sigma_nonempty_of_exists_nonempty`, `card_sigmaLift`, `coe_sigma`, `disjiUnion_map_sigma_mk`, `inf_sigma`, `mem_sigma`, `mem_sigmaLift`, `mk_mem_sigmaLift`, `notMem_sigmaLift_of_ne_left`, `notMem_sigmaLift_of_ne_right`, `pairwiseDisjoint_map_sigmaMk`, `sigmaLift_eq_empty`, `sigmaLift_mono`, `sigmaLift_nonempty`, `sigma_eq_biUnion`, `sigma_eq_empty`, `sigma_mono`, `sigma_nonempty`, `sup_sigma`, `biInter_finsetSigma`, `biInter_finsetSigma'`, `biUnion_finsetSigma`, `biUnion_finsetSigma'`, `biInf_finsetSigma`, `biInf_finsetSigma'`, `biSup_finsetSigma`, `biSup_finsetSigma'`	27
Total	29

Finset

Definitions

Name	Category	Theorems
`sigma` 📖	CompOp	35 math math: `inf_sigma`, `Set.biUnion_finsetSigma`, `sigma_image_fst_preimage_mk`, `sigma_nonempty`, `Set.biUnion_finsetSigma_univ`, `Set.biInter_finsetSigma'`, `Set.biInter_finsetSigma`, `biSup_finsetSigma'`, `sum_sigma`, `Set.biInter_finsetSigma_univ`, `Finmap.sigma_keys_lookup`, `mem_sigma`, `prod_sigma`, `univ_sigma_univ`, `card_sigma`, `biInf_finsetSigma`, `sum_sigma'`, `biInf_finsetSigma'`, `supIndep_sigma_iff'`, `sigma_mono`, `sigma_eq_empty`, `sigma_preimage_mk`, `prod_sigma'`, `sigma_preimage_mk_of_subset`, `sigma_eq_biUnion`, `Set.biUnion_finsetSigma'`, `sup_sigma`, `Set.biUnion_finsetSigma_univ'`, `Finsupp.sigma_support`, `Aesop.sigma_nonempty_of_exists_nonempty`, `coe_sigma`, `Set.biInter_finsetSigma_univ'`, `biSup_finsetSigma`, `disjiUnion_map_sigma_mk`, `SupIndep.sigma`
`sigmaLift` 📖	CompOp	8 math math: `mk_mem_sigmaLift`, `card_sigmaLift`, `mem_sigmaLift`, `sigmaLift_nonempty`, `notMem_sigmaLift_of_ne_left`, `sigmaLift_eq_empty`, `sigmaLift_mono`, `notMem_sigmaLift_of_ne_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_sigmaLift` 📖	mathematical	—	`card` `sigmaLift`	—	`card_map`
`coe_sigma` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `sigma` `Set.sigma`	—	`Set.ext` `mem_sigma`
`disjiUnion_map_sigma_mk` 📖	mathematical	—	`disjiUnion` `map` `Function.Embedding.sigmaMk` `pairwiseDisjoint_map_sigmaMk` `sigma`	—	`pairwiseDisjoint_map_sigmaMk`
`inf_sigma` 📖	mathematical	—	`inf` `sigma`	—	`sup_sigma`
`mem_sigma` 📖	mathematical	—	`Finset` `instMembership` `sigma`	—	`Multiset.mem_sigma`
`mem_sigmaLift` 📖	mathematical	—	`Finset` `instMembership` `sigmaLift`	—	`Decidable.eq_or_ne` `sigmaLift.eq_1` `mem_map` `Sigma.eta` `notMem_empty`
`mk_mem_sigmaLift` 📖	mathematical	—	`Finset` `instMembership` `sigmaLift`	—	`sigmaLift.eq_1` `mem_map`
`notMem_sigmaLift_of_ne_left` 📖	mathematical	—	`Finset` `instMembership` `sigmaLift`	—	`mem_sigmaLift` `Exists.fst`
`notMem_sigmaLift_of_ne_right` 📖	mathematical	—	`Finset` `instMembership` `sigmaLift`	—	`mem_sigmaLift` `Exists.fst` `Exists.snd`
`pairwiseDisjoint_map_sigmaMk` 📖	mathematical	—	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `map` `Function.Embedding.sigmaMk`	—	`Function.onFun.eq_1` `disjoint_left`
`sigmaLift_eq_empty` 📖	mathematical	—	`sigmaLift` `Finset` `instEmptyCollection`	—	`instIsEmptyFalse`
`sigmaLift_mono` 📖	mathematical	`Finset` `instHasSubset`	`sigmaLift`	—	`mem_sigmaLift`
`sigmaLift_nonempty` 📖	mathematical	—	`Nonempty` `sigmaLift`	—	`instIsEmptyFalse`
`sigma_eq_biUnion` 📖	mathematical	—	`sigma` `biUnion` `map` `Function.Embedding.sigmaMk`	—	`ext`
`sigma_eq_empty` 📖	mathematical	—	`sigma` `Finset` `instEmptyCollection`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `Mathlib.Tactic.Push.not_forall_eq` `sigma_nonempty`
`sigma_mono` 📖	mathematical	`Finset` `instHasSubset`	`sigma`	—	`mem_sigma`
`sigma_nonempty` 📖	mathematical	—	`Nonempty` `sigma` `Finset` `instMembership`	—	—
`sup_sigma` 📖	mathematical	—	`sup` `sigma`	—	`LE.le.trans'` `le_sup` `mem_sigma`

Finset.Aesop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigma_nonempty_of_exists_nonempty` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.Nonempty`	`Finset.sigma`	—	`Finset.sigma_nonempty`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_finsetSigma` 📖	mathematical	—	`iInter` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biInf_finsetSigma`
`biInter_finsetSigma'` 📖	mathematical	—	`iInter` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biInf_finsetSigma'`
`biUnion_finsetSigma` 📖	mathematical	—	`iUnion` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biSup_finsetSigma`
`biUnion_finsetSigma'` 📖	mathematical	—	`iUnion` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biSup_finsetSigma'`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInf_finsetSigma` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biSup_finsetSigma`
`biInf_finsetSigma'` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biInf_finsetSigma`
`biSup_finsetSigma` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Finset` `Finset.instMembership` `Finset.sigma`	—	`iSup_congr_Prop` `Finset.coe_sigma` `biSup_sigma`
`biSup_finsetSigma'` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Finset` `Finset.instMembership` `Finset.sigma`	—	`biSup_finsetSigma`

---

← Back to Index