Balanced

📁 Source: Mathlib/CategoryTheory/Functor/ReflectsIso/Balanced.lean

Statistics

Metric	Count
Definitions Balanced, Balanced, Balanced	3
Theorems balanced_of_preserves, reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms	2
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
Balanced 📖	CompData	7 math math: SSet.instBalanced, balanced_of_strongEpiCategory, balanced_of_strongMonoCategory, SheafOfTypes.balanced, SimplexCategory.instBalanced, balanced_opposite, Functor.balanced_of_preserves

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms 📖	mathematical	—	Functor.ReflectsIsomorphisms	—	isIso_of_mono_of_epi Functor.mono_of_mono_map mono_of_strongMono strongMono_of_isIso Functor.epi_of_epi_map epi_of_strongEpi strongEpi_of_isIso

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
balanced_of_preserves 📖	mathematical	—	CategoryTheory.Balanced	—	CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.isIso_of_mono_of_epi map_mono map_epi

Ordnode

Definitions

Name	Category	Theorems
Balanced 📖	MathDef	1 math math: Valid'.bal

(root)

Definitions

Name	Category	Theorems
Balanced 📖	MathDef	19 math math: balanced_empty, balanced_ball_zero, balanced_iff_smul_mem, Seminorm.balanced_closedBall_zero, Seminorm.balanced_ball_zero, nhds_basis_balanced, balanced_neg, balancedCoreAux_balanced, nhds_basis_closed_balanced, balanced_closedBall_zero, balancedCore_balanced, balanced_univ, balancedHull.balanced, mem_balancedCore_iff, balanced_absConvexHull, balanced_iff_closedBall_smul, balanced_iff_neg_mem, AbsConvexOpenSets.coe_balanced, balanced_zero

---

← Back to Index