Structures · Order
DirectedSystem
A directed system is a functor from a category (directed poset) to another category.
- Defined in
- Mathlib.Order.DirectedInverseSystem
- Shape
- 2 explicit arguments · adds map_self, map_map
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Nat
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by282
- DirectLimit
- DirectLimit.setoid
- DirectLimit.lift
- FirstOrder.Language.DirectLimit
- FirstOrder.Language.DirectLimit.of
- DirectLimit.induction
- FirstOrder.Language.DirectLimit.setoid
- DirectLimit.map₀
- DirectLimit.eq_of_le
- DirectLimit.Module.of
- DirectLimit.map₀_def
- DirectLimit.Ring.of
- DirectLimit.NonUnitalStarRing.of
- DirectLimit.induction₂
- DirectLimit.NonUnitalRing.of
- DirectLimit.Algebra.of
- FirstOrder.Language.DirectLimit.lift
- Ring.DirectLimit.ringEquiv
- DirectLimit.Ring.lift
- ModuleCat.directLimitDiagram
- DirectLimit.NonUnitalAlgebra.of
- DirectLimit.map₂_def
- DirectLimit.lift.congr_simp
- DirectLimit.lift_def
- FirstOrder.Language.DirectedSystem.map_self
- DirectLimit.Module.lift
- FirstOrder.Language.DirectLimit.equiv_iff
- Module.DirectLimit.exists_eq_of_of_eq
- DirectedSystem.map_map'
- FirstOrder.Language.DirectLimit.equiv_lift
- ModuleCat.directLimitCocone
- Module.DirectLimit.linearEquiv
- DirectLimit.Algebra.lift
- DirectLimit.NonUnitalStarRing.lift
- DirectLimit.zero_def
- DirectLimit.NonUnitalAlgebra.lift
- DirectLimit.NonUnitalRing.lift
- DirectedSystem.map_self
- DirectLimit.map₂
- DirectedSystem.map_map
- FirstOrder.Language.DirectLimit.comp_unify
- DirectedSystem.map_self'
- DirectLimit.one_def
- DirectLimit.lift₂_def₂
- DirectLimit.mul_def
- DirectLimit.lift₂
- FirstOrder.Language.DirectLimit.inductionOn
- DirectLimit.map
- FirstOrder.Language.DirectedSystem.map_map
- DirectLimit.add_def
Ancestors0
No ancestors.