Theoremsadd_subset, add_subset_closure, closure_add_le, closure_neg, closure_nsmul, closure_nsmul_le, coe_add_self_eq, coe_neg, coe_negOrderIso_apply, coe_negOrderIso_symm_apply, coe_sup, mem_closure_neg, mem_neg, neg_bot, neg_iInf, neg_iSup, neg_inf, neg_le, neg_le_neg, neg_sup, neg_top, nsmul_vadd_mem_closure_vadd, sup_eq_closure_add, addSubmonoid_closure, submonoid_closure, closure_inv, closure_mul_le, closure_pow, closure_pow_le, coe_inv, coe_invOrderIso_apply, coe_invOrderIso_symm_apply, coe_mul_self_eq, coe_pointwise_smul, coe_sup, instCovariantClassHSMulLe, inv_bot, inv_iInf, inv_iSup, inv_inf, inv_le, inv_le_inv, inv_sup, inv_top, mem_closure_inv, mem_inv, mem_inv_pointwise_smul_iff, mem_pointwise_smul_iff_inv_smul_mem, mem_smul_pointwise_iff_exists, mul_subset, mul_subset_closure, pointwise_isCentralScalar, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_subset_iff, pow_smul_mem_closure_smul, smul_bot, smul_closure, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, smul_sup, subset_pointwise_smul_iff, sup_eq_closure_mul, coe_add_coe, coe_mul_coe, coe_set_nsmul, coe_set_pow | 66 |