Documentation Verification Report

W

šŸ“ Source: Mathlib/Data/PFunctor/Multivariate/W.lean

Statistics

MetricCount
DefinitionsW, W, W, W, W, W, W, WPath, inhabited, mvfunctorW, objAppend1, wCases, wDest', wInd, wMap, wMk, wMk', wPathCasesOn, wPathDestLeft, wPathDestRight, wRec, w_cases, w_ind, wp, wpInd, wpMk, wpRec, wp_ind, W, W
30
Theoremscomp_wPathCasesOn, map_objAppend1, wDest'_wMk, wDest'_wMk', wInd_wMk, wMk_eq, wPathCasesOn_eta, wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn, wRec_eq, w_map_wMk, wpRec_eq
12
Total42

CategoryTheory.GrothendieckTopology

Definitions

NameCategoryTheorems
W šŸ“–CompOp
32 mathmath: W_sheafToPresheaf_map_iff_isIso, W_of_isLocallyBijective, W_eq_inverseImage_isomorphisms, CategoryTheory.Sieve.W_shrinkFunctor_Ī¹_of_mem, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W, Point.W_isInvertedBy_presheafFiber', CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints, W.transport_isMonoidal, W_iff_isIso_map_of_adjunction, W_isInvertedBy_whiskeringRight_presheafToSheaf, PreservesSheafification.le, W_adj_unit_app, WEqualsLocallyBijective.iff, W_of_preservesSheafification, W_inverseImage_whiskeringLeft, Point.W_isInvertedBy_presheafFiber, CategoryTheory.Functor.W_map_of_adjunction_of_isContinuous, W.monoidal, PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms, W_whiskerLeft_iff, W.whiskerLeft, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff, instIsLocalizationFunctorOppositeSheafPresheafToSheafW, W_iff, W_eq_inverseImage_isomorphisms_of_adjunction, PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf, W_toSheafify, W_eq_isLocal_range_sheafToPresheaf_obj, W_eq_W_range_sheafToPresheaf_obj, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, W_iff_isLocallyBijective, W.whiskerRight

CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram

Definitions

NameCategoryTheorems
W šŸ“–CompOp
12 mathmath: 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

NameCategoryTheorems
W šŸ“–CompOp
1 mathmath: w

CategoryTheory.Localization.LeftBousfield

Definitions

NameCategoryTheorems
W šŸ“–CompOpā€”

CategoryTheory.NormalEpi

Definitions

NameCategoryTheorems
W šŸ“–CompOp
1 mathmath: w

CategoryTheory.RegularEpi

Definitions

NameCategoryTheorems
W šŸ“–CompOp
2 mathmath: w, w_assoc

MvPFunctor

Definitions

NameCategoryTheorems
W šŸ“–CompOp
8 mathmath: 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 mathmath: comp_wPathCasesOn
mvfunctorW šŸ“–CompOp
2 mathmath: w_map_wMk, MvQPF.wEquiv_map
objAppend1 šŸ“–CompOp
1 mathmath: map_objAppend1
wCases šŸ“–CompOpā€”
wDest' šŸ“–CompOp
3 mathmath: wDest'_wMk', wDest'_wMk, MvQPF.recF_eq'
wInd šŸ“–CompOp
1 mathmath: wInd_wMk
wMap šŸ“–CompOp
1 mathmath: map_objAppend1
wMk šŸ“–CompOp
8 mathmath: wDest'_wMk, wMk_eq, MvQPF.Fix.ind_aux, w_map_wMk, wInd_wMk, wRec_eq, MvQPF.wrepr_wMk, MvQPF.recF_eq
wMk' šŸ“–CompOp
2 mathmath: wDest'_wMk', MvQPF.wrepr_wMk
wPathCasesOn šŸ“–CompOp
5 mathmath: wPathDestLeft_wPathCasesOn, wMk_eq, wPathCasesOn_eta, comp_wPathCasesOn, wPathDestRight_wPathCasesOn
wPathDestLeft šŸ“–CompOp
2 mathmath: wPathDestLeft_wPathCasesOn, wPathCasesOn_eta
wPathDestRight šŸ“–CompOp
3 mathmath: wpRec_eq, wPathCasesOn_eta, wPathDestRight_wPathCasesOn
wRec šŸ“–CompOp
1 mathmath: wRec_eq
w_cases šŸ“–CompOpā€”
w_ind šŸ“–CompOpā€”
wp šŸ“–CompOp
1 mathmath: wMk_eq
wpInd šŸ“–CompOpā€”
wpMk šŸ“–CompOpā€”
wpRec šŸ“–CompOp
1 mathmath: wpRec_eq
wp_ind šŸ“–CompOpā€”

Theorems

NameKindAssumesProvesValidatesDepends 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
wInd_wMk šŸ“–mathematicalā€”wInd
wMk		ā€”ā€”
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_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		ā€”ā€”

MvPFunctor.WPath

Definitions

NameCategoryTheorems
inhabited šŸ“–CompOpā€”

PFunctor

Definitions

NameCategoryTheorems
W šŸ“–CompOp
3 mathmath: QPF.recF_eq', QPF.Fix.ind_aux, QPF.recF_eq

Real.Wallis

Definitions

NameCategoryTheorems
W šŸ“–CompOp
9 mathmath: 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