DenseAt

📁 Source: Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean

Statistics

Metric	Count
Definitions DenseAt, ofIso, ofNatIso, postcompEquivalence, precompEquivOfFinal, precompEquivalence, precompOfFinal, denseAtEquiv, isDenseAt	9
Theorems iff_of_final, of_final, congr_isDenseAt, instIsClosedUnderIsomorphismsIsDenseAt, isDenseAt_eq_isPointwiseLeftKanExtensionAt, isDenseAt_iff	6
Total	15

CategoryTheory.Functor

Definitions

Name	Category	Theorems
DenseAt 📖	CompOp	—
denseAtEquiv 📖	CompOp	—
isDenseAt 📖	CompOp	7 math math: IsDenseAt.iff_of_final, isDenseAt_eq_isPointwiseLeftKanExtensionAt, isDenseAt_iff, congr_isDenseAt, IsDense.isDenseAt, instIsClosedUnderIsomorphismsIsDenseAt, IsDenseAt.of_final

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_isDenseAt 📖	mathematical	—	isDenseAt	—	—
instIsClosedUnderIsomorphismsIsDenseAt 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms isDenseAt	—	isDenseAt_eq_isPointwiseLeftKanExtensionAt LeftExtension.instIsClosedUnderIsomorphismsIsPointwiseLeftKanExtensionAt
isDenseAt_eq_isPointwiseLeftKanExtensionAt 📖	mathematical	—	isDenseAt LeftExtension.isPointwiseLeftKanExtensionAt id CategoryTheory.Iso.inv CategoryTheory.Functor category comp rightUnitor	—	—
isDenseAt_iff 📖	mathematical	—	isDenseAt CategoryTheory.Limits.IsColimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow comp CategoryTheory.CostructuredArrow.proj LeftExtension.coconeAt id CategoryTheory.Iso.inv CategoryTheory.Functor category rightUnitor	—	—

CategoryTheory.Functor.DenseAt

Definitions

Name	Category	Theorems
ofIso 📖	CompOp	—
ofNatIso 📖	CompOp	—
postcompEquivalence 📖	CompOp	—
precompEquivOfFinal 📖	CompOp	—
precompEquivalence 📖	CompOp	—
precompOfFinal 📖	CompOp	—

CategoryTheory.Functor.IsDenseAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_of_final 📖	mathematical	—	CategoryTheory.Functor.isDenseAt CategoryTheory.Functor.comp	—	Equiv.nonempty_congr
of_final 📖	mathematical	—	CategoryTheory.Functor.isDenseAt CategoryTheory.Functor.comp	—	iff_of_final

---

← Back to Index