PairingCore

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean

Statistics

Metric	Count
Definitions pairingCore, PairingCore, AncestralRel, I, IsInner, IsProper, IsRegular, dim, equivI, equivII, index, pairing, simplex, type₁, type₂, ι	16
Theorems ne_last, ne_zero, isUniquelyCodimOneFace, toIsProper, wf, ancestralRel_iff, equivII_apply_coe, equivI_apply_coe, injective_type₁, injective_type₁', injective_type₂, injective_type₂', instIsInnerPairingOfIsInner, instIsProperPairingOfIsProper, instIsRegularPairingOfIsRegular, isUniquelyCodimOneFace, isUniquelyCodimOneFace_index, isUniquelyCodimOneFace_index_coe, nonDegenerate₁, nonDegenerate₂, notMem₁, notMem₂, pairing_I, pairing_II, pairing_p_equivII, pairing_p_symm_equivI, surjective, surjective', type₁_dim, type₁_ne_type₂, type₁_ne_type₂', type₁_simplex, type₂_dim, type₂_simplex	34
Total	50

SSet.Subcomplex

Definitions

Name	Category	Theorems
PairingCore 📖	CompData	—

SSet.Subcomplex.Pairing

Definitions

Name	Category	Theorems
pairingCore 📖	CompOp	—

SSet.Subcomplex.PairingCore

Definitions

Name	Category	Theorems
AncestralRel 📖	MathDef	2 math math: IsRegular.wf, ancestralRel_iff
I 📖	CompOp	4 math math: pairing_p_equivII, pairing_I, equivI_apply_coe, pairing_p_symm_equivI
IsInner 📖	CompData	—
IsProper 📖	CompData	1 math math: IsRegular.toIsProper
IsRegular 📖	CompData	—
dim 📖	CompOp	8 math math: surjective', type₂_dim, type₂_simplex, nonDegenerate₂, type₁_dim, notMem₁, notMem₂, nonDegenerate₁
equivI 📖	CompOp	3 math math: pairing_p_equivII, equivI_apply_coe, pairing_p_symm_equivI
equivII 📖	CompOp	4 math math: pairing_p_equivII, ancestralRel_iff, equivII_apply_coe, pairing_p_symm_equivI
index 📖	CompOp	6 math math: isUniquelyCodimOneFace_index, surjective', isUniquelyCodimOneFace_index_coe, type₂_simplex, nonDegenerate₂, notMem₂
pairing 📖	CompOp	8 math math: instIsInnerPairingOfIsInner, instIsRegularPairingOfIsRegular, pairing_p_equivII, pairing_I, ancestralRel_iff, pairing_II, instIsProperPairingOfIsProper, pairing_p_symm_equivI
simplex 📖	CompOp	7 math math: surjective', type₂_simplex, nonDegenerate₂, notMem₁, type₁_simplex, notMem₂, nonDegenerate₁
type₁ 📖	CompOp	9 math math: isUniquelyCodimOneFace, isUniquelyCodimOneFace_index, isUniquelyCodimOneFace_index_coe, equivI_apply_coe, IsProper.isUniquelyCodimOneFace, type₁_dim, injective_type₁, surjective, type₁_simplex
type₂ 📖	CompOp	9 math math: isUniquelyCodimOneFace, injective_type₂, isUniquelyCodimOneFace_index, isUniquelyCodimOneFace_index_coe, type₂_dim, type₂_simplex, IsProper.isUniquelyCodimOneFace, surjective, equivII_apply_coe
ι 📖	CompOp	8 math math: injective_type₂, IsRegular.wf, pairing_p_equivII, equivI_apply_coe, injective_type₁, ancestralRel_iff, equivII_apply_coe, pairing_p_symm_equivI

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ancestralRel_iff 📖	mathematical	—	AncestralRel SSet.Subcomplex.Pairing.AncestralRel pairing DFunLike.coe Equiv ι Set.Elem SSet.Subcomplex.N II EquivLike.toFunLike Equiv.instEquivLike equivII	—	EquivLike.toEmbeddingLike pairing_p_equivII
equivII_apply_coe 📖	mathematical	—	SSet.Subcomplex.N Set Set.instMembership Set.range ι type₂ DFunLike.coe Equiv Set.Elem II EquivLike.toFunLike Equiv.instEquivLike equivII	—	—
equivI_apply_coe 📖	mathematical	—	SSet.Subcomplex.N Set Set.instMembership Set.range ι type₁ DFunLike.coe Equiv Set.Elem I EquivLike.toFunLike Equiv.instEquivLike equivI	—	—
injective_type₁ 📖	mathematical	—	ι SSet.Subcomplex.N type₁	—	injective_type₁' SSet.N.ext_iff SSet.Subcomplex.N.ext_iff
injective_type₁' 📖	—	dim simplex	—	—	—
injective_type₂ 📖	mathematical	—	ι SSet.Subcomplex.N type₂	—	injective_type₂' SSet.N.ext_iff SSet.Subcomplex.N.ext_iff
injective_type₂' 📖	—	dim CategoryTheory.SimplicialObject.δ CategoryTheory.types index simplex	—	—	—
instIsInnerPairingOfIsInner 📖	mathematical	—	SSet.Subcomplex.Pairing.IsInner pairing instIsProperPairingOfIsProper	—	instIsProperPairingOfIsProper SSet.Subcomplex.Pairing.isUniquelyCodimOneFace Equiv.surjective pairing_p_equivII SSet.S.IsUniquelyCodimOneFace.index.congr_simp isUniquelyCodimOneFace_index IsInner.ne_zero IsInner.ne_last
instIsProperPairingOfIsProper 📖	mathematical	—	SSet.Subcomplex.Pairing.IsProper pairing	—	Equiv.surjective pairing_p_equivII isUniquelyCodimOneFace
instIsRegularPairingOfIsRegular 📖	mathematical	—	SSet.Subcomplex.Pairing.IsRegular pairing	—	instIsProperPairingOfIsProper IsRegular.toIsProper IsRegular.wf wellFounded_iff_isEmpty_descending_chain IsEmpty.false Equiv.apply_symm_apply
isUniquelyCodimOneFace 📖	mathematical	—	SSet.S.IsUniquelyCodimOneFace SSet.N.toS SSet.Subcomplex.N.toN type₂ type₁	—	IsProper.isUniquelyCodimOneFace
isUniquelyCodimOneFace_index 📖	mathematical	—	SSet.S.IsUniquelyCodimOneFace.index SSet.N.toS SSet.Subcomplex.N.toN type₂ type₁ isUniquelyCodimOneFace SSet.S.dim index	—	isUniquelyCodimOneFace SSet.S.IsUniquelyCodimOneFace.δ_eq_iff
isUniquelyCodimOneFace_index_coe 📖	mathematical	dim	SSet.S.IsUniquelyCodimOneFace.index SSet.N.toS SSet.Subcomplex.N.toN type₂ type₁ isUniquelyCodimOneFace index	—	isUniquelyCodimOneFace isUniquelyCodimOneFace_index
nonDegenerate₁ 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op dim Set Set.instMembership SSet.nonDegenerate simplex	—	—
nonDegenerate₂ 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op dim Set Set.instMembership SSet.nonDegenerate CategoryTheory.SimplicialObject.δ index simplex	—	—
notMem₁ 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op dim Set Set.instMembership CategoryTheory.Subfunctor.obj simplex	—	—
notMem₂ 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op dim Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.SimplicialObject.δ index simplex	—	—
pairing_I 📖	mathematical	—	SSet.Subcomplex.Pairing.I pairing I	—	—
pairing_II 📖	mathematical	—	SSet.Subcomplex.Pairing.II pairing II	—	—
pairing_p_equivII 📖	mathematical	—	DFunLike.coe Equiv Set.Elem SSet.Subcomplex.N II I EquivLike.toFunLike Equiv.instEquivLike SSet.Subcomplex.Pairing.p pairing ι equivII equivI	—	Equiv.symm_apply_apply
pairing_p_symm_equivI 📖	mathematical	—	DFunLike.coe Equiv Set.Elem SSet.Subcomplex.N I II EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.Subcomplex.Pairing.II pairing SSet.Subcomplex.Pairing.I SSet.Subcomplex.Pairing.p ι equivI equivII	—	Equiv.symm_apply_apply
surjective 📖	mathematical	—	type₁ type₂	—	surjective' SSet.Subcomplex.N.ext_iff SSet.N.ext_iff
surjective' 📖	mathematical	—	SSet.N.toS SSet.Subcomplex.N.toN dim simplex CategoryTheory.SimplicialObject.δ CategoryTheory.types index	—	—
type₁_dim 📖	mathematical	—	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN type₁ dim	—	—
type₁_ne_type₂ 📖	—	—	—	—	type₁_ne_type₂'
type₁_ne_type₂' 📖	—	—	—	—	—
type₁_simplex 📖	mathematical	—	SSet.S.simplex SSet.N.toS SSet.Subcomplex.N.toN type₁ simplex	—	—
type₂_dim 📖	mathematical	—	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN type₂ dim	—	—
type₂_simplex 📖	mathematical	—	SSet.S.simplex SSet.N.toS SSet.Subcomplex.N.toN type₂ CategoryTheory.SimplicialObject.δ CategoryTheory.types dim index simplex	—	—

SSet.Subcomplex.PairingCore.IsInner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne_last 📖	—	—	—	—	—
ne_zero 📖	—	—	—	—	—

SSet.Subcomplex.PairingCore.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniquelyCodimOneFace 📖	mathematical	—	SSet.S.IsUniquelyCodimOneFace SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.PairingCore.type₂ SSet.Subcomplex.PairingCore.type₁	—	—

SSet.Subcomplex.PairingCore.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsProper 📖	mathematical	—	SSet.Subcomplex.PairingCore.IsProper	—	—
wf 📖	mathematical	—	SSet.Subcomplex.PairingCore.ι SSet.Subcomplex.PairingCore.AncestralRel	—	—

---

← Back to Index