Structures · Algebra
VAddMemClass
VAddMemClass S R M says S is a type of subsets s ≤ M that are closed under the
additive action of R on M.
Note that only R is marked as an outParam here, since M is supplied by the SetLike
class instead.
- Shape
- 3 explicit arguments · adds vadd_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- SubAddAction
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- VAddMemClass.vadd_mem
- SubAddAction.SMulMemClass.subtype
- SetLike.val_vadd
- SetLike.vadd_subset_self
- SetLike.vadd'
- SetLike.addUnits_vadd
- RestrictedProduct.instVAddCoeOfVAddMemClass
- SubAddAction.SMulMemClass.toAddAction
- SetLike.mk_vadd_of_tower_mk
- SetLike.val_vadd_of_tower
- RestrictedProduct.vadd_apply
- RestrictedProduct.continuousVAdd
- SetLike.instVAddCommClassSubtypeMem_1
- SetLike.vadd
- SetLike.instVAddCommClassSubtypeMem
- RestrictedProduct.instContinuousConstVAddCoe
- SetLike.vadd_def
- SubAddAction.SMulMemClass.coe_subtype
- SetLike.vadd_of_tower_def
- SetLike.instIsLeftCancelVAddSubtypeMem
- VAddMemClass.continuousVAdd
- RestrictedProduct.instContinuousVAddCoePrincipal
- SetLike.mk_vadd_mk
- VAddMemClass.ofVAddAssocClass
- SetLike.instIsCancelVAddSubtypeMem
- SetLike.instVAddCommClassSubtypeMem_2
Ancestors0
No ancestors.