Documentation Verification Report

W

📁 Source: Mathlib/Data/PFunctor/Multivariate/W.lean

Statistics

Metric	Count
Definitions `W`, `W`, `W`, `W`, `W`, `W`, `W`, `WPath`, `inhabited`, `mvfunctorW`, `objAppend1`, `wDest'`, `wMap`, `wMk`, `wMk'`, `wPathCasesOn`, `wPathDestLeft`, `wPathDestRight`, `wRec`, `wp`, `wpMk`, `wpRec`, `W`, `W`	24
Theorems `comp_wPathCasesOn`, `map_objAppend1`, `wDest'_wMk`, `wDest'_wMk'`, `wMk_eq`, `wPathCasesOn_eta`, `wPathDestLeft_wPathCasesOn`, `wPathDestRight_wPathCasesOn`, `wRec_eq`, `w_cases`, `w_ind`, `w_map_wMk`, `wpRec_eq`, `wp_ind`	14
Total	38

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`W` 📖	CompOp	21 math math: `W_sheafToPresheaf_map_iff_isIso`, `W_of_isLocallyBijective`, `W_eq_inverseImage_isomorphisms`, `W.transport_isMonoidal`, `W_iff_isIso_map_of_adjunction`, `W_isInvertedBy_whiskeringRight_presheafToSheaf`, `PreservesSheafification.le`, `W_adj_unit_app`, `WEqualsLocallyBijective.iff`, `W_inverseImage_whiskeringLeft`, `Point.W_isInvertedBy_presheafFiber`, `W.monoidal`, `W_whiskerLeft_iff`, `instIsLocalizationFunctorOppositeSheafPresheafToSheafW`, `W_iff`, `W_eq_inverseImage_isomorphisms_of_adjunction`, `W_toSheafify`, `W_eq_isLocal_range_sheafToPresheaf_obj`, `W_eq_W_range_sheafToPresheaf_obj`, `LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology`, `W_iff_isLocallyBijective`

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram

Definitions

Name	Category	Theorems
`W` 📖	CompOp	12 math math: `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext_iff`, `IsTerminal.hlift`, `ext_iff`, `iSup_W`, `IsTerminal.prop_id`, `single_W`, `hW`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W`, `sup_W`

CategoryTheory.IsRegularEpi

Definitions

Name	Category	Theorems
`W` 📖	CompOp	1 math math: `w`

CategoryTheory.Localization.LeftBousfield

Definitions

Name	Category	Theorems
`W` 📖	CompOp	—

CategoryTheory.NormalEpi

Definitions

Name	Category	Theorems
`W` 📖	CompOp	1 math math: `w`

CategoryTheory.RegularEpi

Definitions

Name	Category	Theorems
`W` 📖	CompOp	2 math math: `w`, `w_assoc`

MvPFunctor

Definitions

Name	Category	Theorems
`W` 📖	CompOp	8 math math: `wDest'_wMk`, `MvQPF.Fix.ind_aux`, `w_map_wMk`, `MvQPF.recF_eq'`, `map_objAppend1`, `MvQPF.wrepr_wMk`, `MvQPF.recF_eq`, `MvQPF.wEquiv_map`
`WPath` 📖	CompData	1 math math: `comp_wPathCasesOn`
`mvfunctorW` 📖	CompOp	2 math math: `w_map_wMk`, `MvQPF.wEquiv_map`
`objAppend1` 📖	CompOp	1 math math: `map_objAppend1`
`wDest'` 📖	CompOp	3 math math: `wDest'_wMk'`, `wDest'_wMk`, `MvQPF.recF_eq'`
`wMap` 📖	CompOp	1 math math: `map_objAppend1`
`wMk` 📖	CompOp	7 math math: `wDest'_wMk`, `wMk_eq`, `MvQPF.Fix.ind_aux`, `w_map_wMk`, `wRec_eq`, `MvQPF.wrepr_wMk`, `MvQPF.recF_eq`
`wMk'` 📖	CompOp	2 math math: `wDest'_wMk'`, `MvQPF.wrepr_wMk`
`wPathCasesOn` 📖	CompOp	5 math math: `wPathDestLeft_wPathCasesOn`, `wMk_eq`, `wPathCasesOn_eta`, `comp_wPathCasesOn`, `wPathDestRight_wPathCasesOn`
`wPathDestLeft` 📖	CompOp	2 math math: `wPathDestLeft_wPathCasesOn`, `wPathCasesOn_eta`
`wPathDestRight` 📖	CompOp	3 math math: `wpRec_eq`, `wPathCasesOn_eta`, `wPathDestRight_wPathCasesOn`
`wRec` 📖	CompOp	1 math math: `wRec_eq`
`wp` 📖	CompOp	1 math math: `wMk_eq`
`wpMk` 📖	CompOp	—
`wpRec` 📖	CompOp	1 math math: `wpRec_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_wPathCasesOn` 📖	mathematical	—	`TypeVec.comp` `WPath` `PFunctor.A` `last` `PFunctor.B` `wPathCasesOn` `B` `drop`	—	`TypeVec.Arrow.ext`
`map_objAppend1` 📖	mathematical	—	`MvFunctor.map` `Obj` `instMvFunctorObj` `TypeVec.append1` `W` `TypeVec.appendFun` `wMap` `objAppend1` `TypeVec.comp` `B` `drop`	—	`objAppend1.eq_1` `map_eq` `TypeVec.appendFun.eq_1` `TypeVec.splitFun_comp`
`wDest'_wMk` 📖	mathematical	—	`wDest'` `wMk` `A` `TypeVec.Arrow` `B` `TypeVec.append1` `W` `TypeVec.splitFun`	—	`wDest'.eq_1` `wRec_eq`
`wDest'_wMk'` 📖	mathematical	—	`wDest'` `wMk'`	—	`wMk'.eq_1` `wDest'_wMk` `TypeVec.split_dropFun_lastFun`
`wMk_eq` 📖	mathematical	—	`wMk` `A` `wp` `TypeVec.Arrow` `B` `PFunctor.A` `last` `PFunctor.B` `wPathCasesOn`	—	—
`wPathCasesOn_eta` 📖	mathematical	—	`wPathCasesOn` `wPathDestLeft` `wPathDestRight`	—	`TypeVec.Arrow.ext`
`wPathDestLeft_wPathCasesOn` 📖	mathematical	—	`wPathDestLeft` `wPathCasesOn`	—	—
`wPathDestRight_wPathCasesOn` 📖	mathematical	—	`wPathDestRight` `wPathCasesOn`	—	—
`wRec_eq` 📖	mathematical	—	`wRec` `wMk`	—	—
`w_cases` 📖	—	`wMk`	—	—	`w_ind`
`w_ind` 📖	—	`wMk`	—	—	`wp_ind` `wPathCasesOn_eta`
`w_map_wMk` 📖	mathematical	—	`MvFunctor.map` `W` `mvfunctorW` `wMk` `TypeVec.comp` `B` `drop`	—	`wMk_eq` `map_eq` `comp_wPathCasesOn`
`wpRec_eq` 📖	mathematical	—	`wpRec` `PFunctor.A` `last` `PFunctor.B` `wPathDestRight`	—	—
`wp_ind` 📖	—	`PFunctor.A` `last` `PFunctor.B`	—	—	—

MvPFunctor.WPath

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

PFunctor

Definitions

Name	Category	Theorems
`W` 📖	CompOp	3 math math: `QPF.recF_eq'`, `QPF.Fix.ind_aux`, `QPF.recF_eq`

Real.Wallis

Definitions

Name	Category	Theorems
`W` 📖	CompOp	9 math math: `W_le`, `tendsto_W_nhds_pi_div_two`, `W_eq_integral_sin_pow_div_integral_sin_pow`, `W_eq_factorial_ratio`, `Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq`, `W_succ`, `W_pos`, `Stirling.second_wallis_limit`, `le_W`

---

← Back to Index