Lemmas

📁 Source: Mathlib/CategoryTheory/WithTerminal/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsFilteredOfIsFilteredOrEmpty, instIsCofilteredOfIsCofilteredOrEmpty	2
Total	2

CategoryTheory.WithInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsFilteredOfIsFilteredOrEmpty 📖	mathematical	—	CategoryTheory.IsFiltered CategoryTheory.WithInitial instCategory	—	CategoryTheory.IsCofiltered.of_equivalence CategoryTheory.WithTerminal.instIsCofilteredOfIsCofilteredOrEmpty CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty CategoryTheory.isFiltered_of_isCofiltered_op

CategoryTheory.WithTerminal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCofilteredOfIsCofilteredOrEmpty 📖	mathematical	—	CategoryTheory.IsCofiltered CategoryTheory.WithTerminal instCategory	—	isIso_of_from_star CategoryTheory.IsIso.eq_comp_inv Unique.instSubsingleton CategoryTheory.IsCofiltered.eq_condition

---

← Back to Index