Elementwise

📁 Source: Mathlib/CategoryTheory/Elementwise.lean

Statistics

Metric	Count
Definitions	0
Theorems hom_inv_id_apply, inv_hom_id_apply, hom_inv_id_apply, inv_hom_id_apply	4
Total	4

CategoryTheory.IsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.inv	—	CategoryTheory.comp_apply CategoryTheory.id_apply Mathlib.Tactic.Elementwise.hom_elementwise hom_inv_id
inv_hom_id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.inv	—	CategoryTheory.comp_apply CategoryTheory.id_apply Mathlib.Tactic.Elementwise.hom_elementwise inv_hom_id

CategoryTheory.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom inv hom	—	CategoryTheory.comp_apply CategoryTheory.id_apply Mathlib.Tactic.Elementwise.hom_elementwise hom_inv_id
inv_hom_id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom hom inv	—	CategoryTheory.comp_apply CategoryTheory.id_apply Mathlib.Tactic.Elementwise.hom_elementwise inv_hom_id

---

← Back to Index