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	2 math math: Valid'.bal, Balanced.dual

(root)

Definitions

Name	Category	Theorems
Balanced 📖	MathDef	35 math math: balanced_iUnion₂, Balanced.sub, balanced_empty, balanced_ball_zero, Balanced.convexHull, balanced_iff_smul_mem, Seminorm.balanced_closedBall_zero, Balanced.sInter, Balanced.add, balanced_iInter, Seminorm.balanced_ball_zero, nhds_basis_balanced, balanced_neg, Balanced.closure, Balanced.interior, balancedCoreAux_balanced, Balanced.smul, Balanced.inter, balanced_iInter₂, Balanced.zero_insert_interior, nhds_basis_closed_balanced, balanced_closedBall_zero, Balanced.union, balancedCore_balanced, balanced_univ, Balanced.neg, Balanced.mulActionHom_preimage, balancedHull.balanced, mem_balancedCore_iff, balanced_absConvexHull, balanced_iff_closedBall_smul, balanced_iUnion, balanced_iff_neg_mem, AbsConvexOpenSets.coe_balanced, balanced_zero

---

← Back to Index