Pairing

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

Statistics

Metric	Count
Definitions AncestralRel, I, IsInner, IsProper, IsRegular, p	6
Theorems dim_le, ne_last, ne_zero, isUniquelyCodimOneFace, toIsProper, wf, dim_p, exists_or, instIsWellFoundedElemNIIAncestralRel, inter, isUniquelyCodimOneFace, ne, union, wf	14
Total	20

SSet.Subcomplex.Pairing

Definitions

Name	Category	Theorems
AncestralRel 📖	MathDef	7 math math: instFiniteSubtypeElemNIIAncestralRel, WeakRankFunction.wf_ancestralRel, RankFunction.wf_ancestralRel, IsRegular.wf, SSet.Subcomplex.PairingCore.ancestralRel_iff, instIsWellFoundedElemNIIAncestralRel, wf
I 📖	CompOp	8 math math: IsProper.isUniquelyCodimOneFace, dim_p, isUniquelyCodimOneFace, SSet.Subcomplex.PairingCore.pairing_I, union, exists_or, inter, SSet.Subcomplex.PairingCore.pairing_p_symm_equivI
IsInner 📖	CompData	1 math math: SSet.Subcomplex.PairingCore.instIsInnerPairingOfIsInner
IsProper 📖	CompData	2 math math: IsRegular.toIsProper, SSet.Subcomplex.PairingCore.instIsProperPairingOfIsProper
IsRegular 📖	CompData	5 math math: SSet.Subcomplex.PairingCore.instIsRegularPairingOfIsRegular, RankFunction.isRegular, WeakRankFunction.isRegular, isRegular_iff_nonempty_weakRankFunction, isRegular_iff_nonempty_rankFunction
p 📖	CompOp	6 math math: IsProper.isUniquelyCodimOneFace, dim_p, isUniquelyCodimOneFace, SSet.Subcomplex.PairingCore.pairing_p_equivII, exists_or, SSet.Subcomplex.PairingCore.pairing_p_symm_equivI

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dim_p 📖	mathematical	—	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership I DFunLike.coe Equiv Set.Elem II EquivLike.toFunLike Equiv.instEquivLike p	—	SSet.S.IsUniquelyCodimOneFace.dim_eq isUniquelyCodimOneFace
exists_or 📖	mathematical	—	SSet.Subcomplex.N Set Set.instMembership II I DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike p	—	Set.mem_univ Set.mem_union union Equiv.surjective
instIsWellFoundedElemNIIAncestralRel 📖	mathematical	—	IsWellFounded Set.Elem SSet.Subcomplex.N II AncestralRel	—	wf
inter 📖	mathematical	—	Set SSet.Subcomplex.N Set.instInter I II Set.instEmptyCollection	—	—
isUniquelyCodimOneFace 📖	mathematical	—	SSet.S.IsUniquelyCodimOneFace SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership II I DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike p	—	IsProper.isUniquelyCodimOneFace
ne 📖	—	—	—	—	inter
union 📖	mathematical	—	Set SSet.Subcomplex.N Set.instUnion I II Set.univ	—	—
wf 📖	mathematical	—	Set.Elem SSet.Subcomplex.N II AncestralRel	—	IsRegular.wf

SSet.Subcomplex.Pairing.AncestralRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dim_le 📖	mathematical	SSet.Subcomplex.Pairing.AncestralRel	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership SSet.Subcomplex.Pairing.II	—	SSet.S.IsUniquelyCodimOneFace.dim_eq SSet.Subcomplex.Pairing.isUniquelyCodimOneFace SSet.N.dim_lt_of_lt

SSet.Subcomplex.Pairing.IsInner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne_last 📖	—	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership SSet.Subcomplex.Pairing.II	—	—	—
ne_zero 📖	—	SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership SSet.Subcomplex.Pairing.II	—	—	—

SSet.Subcomplex.Pairing.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniquelyCodimOneFace 📖	mathematical	—	SSet.S.IsUniquelyCodimOneFace SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership SSet.Subcomplex.Pairing.II SSet.Subcomplex.Pairing.I DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike SSet.Subcomplex.Pairing.p	—	—

SSet.Subcomplex.Pairing.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsProper 📖	mathematical	—	SSet.Subcomplex.Pairing.IsProper	—	—
wf 📖	mathematical	—	Set.Elem SSet.Subcomplex.N SSet.Subcomplex.Pairing.II SSet.Subcomplex.Pairing.AncestralRel	—	—

---

← Back to Index