Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `decidableEq`, `elim`, `instInhabitedOfDefault_mathlib`, `map`, `toSigma`, `curry`, `instDecidableEqSigma`, `instInhabitedSigma`, `map`, `uncurry`	10
Theorems `of_sigma_map`, `sigma_map`, `sigma_map_iff`, `sigma_map`, `eq_of_sigmaMk_comp`, `elim_val`, `exists`, `forall`, `inj_iff`, `subtype_ext`, `subtype_ext_iff`, `fst_comp_toSigma`, `fst_toSigma`, `snd_toSigma`, `toSigma_inj`, `toSigma_injective`, `toSigma_mk`, `curry_uncurry`, `curry_update`, `eq`, `eta`, `exists`, `exists'`, `forall`, `forall'`, `fst_injective`, `fst_injective_iff`, `fst_surjective`, `fst_surjective_iff`, `map_mk`, `inj_iff`, `subtype_ext`, `subtype_ext_iff`, `uncurry_curry`, `sigma_mk_injective`	35
Total	45

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_sigmaMk_comp` 📖	—	—	—	—	—

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_sigma_map` 📖	—	`Sigma.map`	—	—	`sigma_mk_injective`
`sigma_map` 📖	mathematical	—	`Sigma.map`	—	`sigma_mk_injective`
`sigma_map_iff` 📖	mathematical	—	`Sigma.map`	—	`of_sigma_map` `sigma_map`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigma_map` 📖	mathematical	—	`Sigma.map`	—	`forall`

PSigma

Definitions

Name	Category	Theorems
`decidableEq` 📖	CompOp	—
`elim` 📖	CompOp	1 math math: `elim_val`
`instInhabitedOfDefault_mathlib` 📖	CompOp	—
`map` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim_val` 📖	mathematical	—	`elim`	—	—
`exists` 📖	—	—	—	—	—
`forall` 📖	—	—	—	—	—
`subtype_ext` 📖	—	—	—	—	—
`subtype_ext_iff` 📖	—	—	—	—	`subtype_ext`

PSigma.mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inj_iff` 📖	—	—	—	—	—

Prod

Definitions

Name	Category	Theorems
`toSigma` 📖	CompOp	8 math math: `fst_comp_toSigma`, `toSigma_injective`, `Matrix.blockDiagonal'_submatrix_eq_blockDiagonal`, `fst_toSigma`, `toSigma_inj`, `Finsupp.toAList_entries`, `toSigma_mk`, `snd_toSigma`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_comp_toSigma` 📖	mathematical	—	`toSigma`	—	—
`fst_toSigma` 📖	mathematical	—	`toSigma`	—	—
`snd_toSigma` 📖	mathematical	—	`toSigma`	—	—
`toSigma_inj` 📖	mathematical	—	`toSigma`	—	`toSigma_injective`
`toSigma_injective` 📖	mathematical	—	`toSigma`	—	—
`toSigma_mk` 📖	mathematical	—	`toSigma`	—	—

Sigma

Definitions

Name	Category	Theorems
`curry` 📖	CompOp	19 math math: `MeasurableEquiv.piCurry_apply`, `curry_update`, `LinearEquiv.piCurry_apply`, `curry_neg`, `measurable_sigmaCurry`, `LinearIsometryEquiv.piLpCurry_apply`, `MultilinearMap.compMultilinearMap_apply`, `curry_single`, `curry_uncurry`, `curry_one`, `curry_zero`, `curry_inv`, `Pi.monotoneCurry_coe`, `Equiv.piCurry_apply`, `curry_add`, `uncurry_curry`, `MeasurableEquiv.coe_piCurry`, `curry_mul`, `curry_mulSingle`
`instDecidableEqSigma` 📖	CompOp	16 math math: `Matrix.blockDiag'_diagonal`, `DFinsupp.sigmaUncurry_single`, `Matrix.blockDiagonal'RingHom_apply`, `curry_update`, `Matrix.blockDiagonal'_one`, `DFinsupp.sigmaCurry_single`, `Matrix.blockDiagonal'_diagonal`, `Matrix.blockDiag'_one`, `curry_single`, `uncurry_mulSingle_mulSingle`, `LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal'`, `uncurry_single_single`, `Matrix.exp_blockDiagonal'`, `LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne`, `curry_mulSingle`, `Matrix.blockDiagonal'_pow`
`instInhabitedSigma` 📖	CompOp	—
`map` 📖	CompOp	26 math math: `CategoryTheory.Presieve.uncurry_bind`, `Function.Injective.sigma_map_iff`, `List.NodupKeys.map₁`, `List.dlookup_map₁`, `continuous_sigma_map`, `List.dlookup_map₂`, `isOpenMap_sigma_map`, `Equiv.sigmaSumDistrib_symm_apply`, `Topology.isInducing_sigmaMap`, `List.dlookup_map`, `Topology.isEmbedding_sigmaMap`, `IsHomeomorph.sigmaMap`, `Continuous.sigma_map`, `Set.image_sigmaMk_preimage_sigmaMap_subset`, `Function.Injective.sigma_map`, `Filter.map_sigma_mk_comap`, `Set.preimage_sigmaMap_sigma`, `List.NodupKeys.map₂`, `Set.image_sigmaMk_preimage_sigmaMap`, `vadd_def`, `map_mk`, `Function.Surjective.sigma_map`, `Topology.isOpenEmbedding_sigmaMap`, `smul_def`, `List.map₂_keys`, `Function.Embedding.sigmaMap_apply`
`uncurry` 📖	CompOp	18 math math: `measurable_sigmaUncurry`, `uncurry_inv`, `uncurry_neg`, `curry_uncurry`, `uncurry_mulSingle_mulSingle`, `uncurry_add`, `Pi.monotoneUncurry_coe`, `LinearIsometryEquiv.piLpCurry_symm_apply`, `MeasurableEquiv.piCurry_symm_apply`, `LinearEquiv.piCurry_symm_apply`, `uncurry_single_single`, `Set.uncurry_preimage_sigma_pi`, `uncurry_curry`, `Equiv.piCurry_symm_apply`, `uncurry_one`, `MeasurableEquiv.coe_piCurry_symm`, `uncurry_zero`, `uncurry_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curry_uncurry` 📖	mathematical	—	`curry` `uncurry`	—	—
`curry_update` 📖	mathematical	—	`curry` `Function.update` `instDecidableEqSigma`	—	`eq_or_ne` `Function.update_self` `Function.update_of_ne`
`eq` 📖	—	—	—	—	—
`eta` 📖	—	—	—	—	—
`exists` 📖	—	—	—	—	—
`exists'` 📖	—	—	—	—	`exists`
`forall` 📖	—	—	—	—	—
`forall'` 📖	—	—	—	—	`forall`
`fst_injective` 📖	—	—	—	—	—
`fst_injective_iff` 📖	—	—	—	—	`sigma_mk_injective` `fst_injective`
`fst_surjective` 📖	—	—	—	—	—
`fst_surjective_iff` 📖	—	—	—	—	`fst_surjective`
`map_mk` 📖	mathematical	—	`map`	—	—
`subtype_ext` 📖	—	—	—	—	—
`subtype_ext_iff` 📖	—	—	—	—	`subtype_ext`
`uncurry_curry` 📖	mathematical	—	`uncurry` `curry`	—	—

Sigma.mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inj_iff` 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigma_mk_injective` 📖	—	—	—	—	—

---

← Back to Index