| Name | Category | Theorems |
|---|
smul π | CompOp | 103 mathmath: Nonempty.zero_smul, inter_smul_union_subset_union, mem_smul, singleton_smul_singleton, Submodule.set_smul_span, set_smul_closure_subset, Seminorm.ball_smul_closedBall, zero_smul_subset, iInterβ_smul_subset, MeasureTheory.Measure.toSphere_apply_aux, Filter.le_smul_iff, sInter_smul_subset, Submodule.smul_mem_span_smul, IsClosed.smul_left_of_isCompact, iInter_smul_subset, tangentConeAt_eq_biInter_closure, Filter.smul_mem_smul, smulCommClass, Finite.smul, Finset.support_smulAntidiagonal_subset_smul, smul_empty, Seminorm.closedBall_smul_ball, Nonempty.smul, iUnion_smul, smul_sInter_subset, op_smul_set_smul_eq_smul_smul_set, smul_mem_smul, set_smul_sphere_zero, inter_smul_subset, smul_univβ, Submodule.smul_subset_smul, Submodule.smul_mem_span_smul_of_mem, singleton_smul, smul_subset_iff, Ioo_smul_sphere_zero, smul_subset_smul_left, Filter.mem_smul, smul_eq_empty, range_smul_range, toFinset_smul, zero_mem_smul_iff, univ_smul_nhds_zero, neg_smul, Nonempty.smul_zero, IsWF.min_smul, IsOpen.smul_sphere, smul_set_subset_smul, Submodule.span_set_smul, MeasureTheory.Measure.toSphere_apply', iUnion_smul_right_image, Submodule.span_eq_closure, iUnion_smul_set, IsPWO.smul, smul_iInter_subset, SeminormFamily.basisSets_smul, image_smul_prod, smulCommClass_set', union_smul, Finite.toFinset_smul, Filter.HasBasis.smul, image2_smul, IsClosed.smul_right_of_isCompact, Seminorm.ball_smul_ball, smul_univ, smul_nonempty, smul_set_closure_subset, ModuleFilterBasis.smul', sUnion_smul, IsWF.smul, Submodule.mem_smul_span, smul_union, AddSubmonoid.smul_subset_smul, smul_inter_subset, smul_iUnionβ, image_op_smul, IsOpen.smul_left, subset_interior_smul_right, smul_zero_subset, smul_singleton, smul_subset_smul, smul_neg, smul_subset_smul_right, subset_interior_smul, IsCompact.smul_set, smul_iUnion, ModuleFilterBasis.smul, smulCommClass_set'', empty_smul, union_smul_inter_subset_union, Submodule.span_smul_span, Filter.HasBasis.tangentConeAt_eq_biInter_closure, smul_sUnion, Finset.coe_smul, smul_iInterβ_subset, iUnion_smul_left_image, iUnionβ_smul, smul_univβ', balanced_iff_closedBall_smul, isScalarTower'', Seminorm.closedBall_smul_closedBall, Submodule.span_smul_of_span_eq_top, smul_singleton_mem_nhds_of_sigmaCompact, isScalarTower'
|
smulSet π | CompOp | 526 mathmath: DoubleCoset.doubleCoset_union_rightCoset, GrpCat.SurjectiveOfEpiAuxs.Ο_apply_fromCoset, interior_smulβ, smul_set_iUnionβ, IsLowerSet.smul, MulAction.IsTrivialBlock.smul, Real.sSup_smul_of_nonpos, smul_set_symmDiff, mul_ball, Bornology.isVonNBounded_iff_tendsto_smallSets_nhds, Submodule.smul_def, Metric.smul_ball, tendsto_tsum_div_pow_atTop_integral, MeasureTheory.measure_sdiff_inv_smul, image_smul_setββ, IsClosed.smul_of_ne_zero, Subgroup.coe_pointwise_smul, bddBelow_smul_iff_of_neg, MulAction.IsBlock.of_subset, Balanced.smul_congr, smul_set_neg, smul_set_subset_mul, MonoidHom.preimage_smul_setββ, mem_own_rightCoset, support_comp_inv_smulβ, smul_mem_nhds_smulβ, image_smul, smul_graphOn_univ, MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one, natCard_smul_setβ, SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj, IsClosed.smulβ, NormedSpace.isBounded_iff_subset_smul_ball, infinite_smul_set, diam_smulβ, smul_balancedCore_subset, smul_set_sUnion, Finset.doubling_lt_three_halves, mem_smul_set_inv, Ideal.smul_closure, IsCompact.closedBall_mul, MulAction.Supports.smul, MeasureTheory.pairwise_disjoint_fundamentalInterior, Dense.smul, mem_leftCoset_iff, EMetric.smul_ball, smul_set_inter, Sylow.coe_smul, DoubleCoset.doubleCoset_union_leftCoset, MeasureTheory.Measure.domSMul_apply, mem_inv_smul_set_iffβ, finite_smul_set, preimage_smul_invβ, MulAction.mem_aestabilizer, smul_set_interβ, lowerBounds_smul_of_pos, smul_set_subset_smul_set_iffβ, hasFDerivWithinAt_comp_smul_iff_smul, MeasureTheory.mem_fundamentalInterior, MeasureTheory.mem_fundamentalFrontier, GrpCat.SurjectiveOfEpiAuxs.Ο_symm_apply_infinity, Submodule.span_smul_eq_of_isUnit, smul_unitClosedBall, MulAction.isBlock_iff_smul_eq_of_mem, MeasureTheory.IsFundamentalDomain.nullMeasurableSet_smul, mulSupport_comp_inv_smul, Convex.set_combo_subset, GrpCat.SurjectiveOfEpiAuxs.Ο_apply_infinity, one_leftCoset, LinearOrderedField.smul_Iio, smul_unitClosedBall_of_nonneg, MeasureTheory.fundamentalFrontier_smul, MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero, Subalgebra.coe_pointwise_smul, MulAction.smul_zpow_movedBy_eq_of_commute, smul_set_inter_subset, image_smul_distrib, UniqueDiffWithinAt.smul, NormedSpace.isBounded_iff_subset_smul_closedBall, rightCoset_eq_iff, MulAction.le_stabilizer_iff_smul_le, MeasureTheory.measure_smul_eq_zero_iff, op_smul_set_smul_eq_smul_smul_set, Real.sInf_smul_of_nonneg, gauge_le_eq, Metric.smul_closedEBall, ediam_smul_le, MulAction.IsBlock.disjoint_smul_of_ne, Absorbent.gauge_set_nonempty, NonarchimedeanRing.left_mul_subset, BoxIntegral.unitPartition.integralSum_eq_tsum_div, MeasureTheory.eventuallyConst_smul_set_ae, smul_set_empty, MulAction.isBlock_iff_smul_eq_or_disjoint, Real.sSup_smul_of_nonneg, tendsto_card_div_pow_atTop_volume, MulAction.op_smul_set_stabilizer_subset, Submodule.span_smul_le, smul_closedBall', closure_smulβ, exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul, Convex.combo_interior_closure_subset_interior, EMetric.infEdist_smul, closure_smulβ', MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1, mem_smul_of_egauge_lt, Submonoid.coe_pointwise_smul, smul_set_insert, IsOpen.iUnion_smul, Seminorm.ball_norm_mul_subset, ZLattice.covolume.tendsto_card_div_pow, IsCompact.exists_finite_cover_smul, smul_set_univβ, IsFoelner.tendsto_meas_smul_symmDiff, LinearOrderedField.smul_Ico, affinity_unitClosedBall, AffineSubspace.coe_smul, mem_balancedCoreAux_iff, pair_mul, MeasureTheory.measure_inv_smul_sdiff, smul_ball'', IsLocalizedModule.finsetIntegerMultiple_image, smul_closedBall_one, smul_set_iInter_subset, Subring.coe_pointwise_smul, OrdConnected.smul, smul_preimage_set_subset, smul_set_pi, Subgroup.leftCoset_cover_const_iff_surjOn, NonarchimedeanGroup.exists_openSubgroup_separating, ball_mul, leftCoset_assoc, IsCompact.div_closedBall, mem_smul_set, QuotientGroup.eq_class_eq_leftCoset, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum_of_ac, singleton_smul, ConvexBody.coe_smul, Convex.combo_self_interior_subset_interior, infEDist_smulβ, MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum', isCentralScalar, Seminorm.smul_closedBall_zero, approxOrderOf.smul_subset_of_coprime, MulAction.isPreprimitive_ofFixingSubgroup_conj_iff, smul_sphere', disjoint_smul_set, MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum, MeasureTheory.IsFundamentalDomain.sum_restrict, smul_set_iInterβ_subset, image_smul_set, MeasureTheory.Measure.hausdorffMeasure_smulβ, smul_coe_set, QuotientGroup.univ_eq_iUnion_smul, le_egauge_smul_left, smul_set_pi_of_surjective, leftCoset_eq_iff, smul_mem_smul_set_iffβ, IsLocalization.finsetIntegerMultiple_image, MulAction.smul_subset_of_set_mem_fixedBy, GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range, MeasureTheory.IsFundamentalDomain.pairwise_aedisjoint_of_ac, IsFoelner.mean_smul_eq_mean_smul, MulAction.smul_orbit, BddAbove.smul_of_nonneg, ncard_smul_set, starConvex_iff_pointwise_add_subset, op_smul_coe_set, smul_upperBounds_subset_upperBounds_smul_of_nonneg, StarConvex.zero_smul, div_ball, smul_eq_self_of_preimage_zpow_eq_self, zero_mem_smul_set_iff, MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq, Submodule.coe_pointwise_smul, Balanced.subset_smul, interior_smul, Bornology.IsVonNBounded.tendsto_smallSets_nhds, MeasureTheory.IsFundamentalDomain.restrict_restrict, MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum, set_smul_mem_nhds_zero_iff, affinity_unitBall, preimage_smul_setββ_of_isUnit_isUnit, IsCompact.mul_closedBall, eventually_singleton_add_smul_subset, IsUnit.smul_mem_nhds_smul_iff, StrictConvex.affinity, Cardinal.mk_smul_set, Absorbs.eventually, mem_invOf_smul_set, BddBelow.smul_of_nonpos, Convex.combo_interior_self_subset_interior, MulAction.IsBlock.of_subgroup_of_conjugate, MulAction.smul_orbit_subset, smul_sphere, MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2, subset_smul_set_iff, MulAction.mem_stabilizer_set_iff_subset_smul_set, IsCompact.closedBall_div, ball_div, DiscreteTiling.PlacedTile.coe_mk_mk, smul_set_mono, upperBounds_smul_of_neg, infEdist_smulβ, subsingleton_zero_smul_set, Convex.smul, ThreeGPFree.smul_setβ, MeasureTheory.measure_symmDiff_inv_smul, MulAction.smul_set_stabilizer_subset, MulAction.isBlock_iff_smul_eq_smul_of_nonempty, fderivWithin_comp_smul_eq_fderivWithin_smul, mem_rightCoset, smul_mem_nhds_self, normal_iff_eq_cosets, isSimplyConnected_smul_set_iff, Finite.toFinset_smul_set, Subring.smul_closure, IsOpen.leftCoset, MeasureTheory.measure_inter_inv_smul, smul_set_subset_smul, MeasureTheory.Measure.NullMeasurableSet.const_smul, hasFDerivWithinAt_comp_smul_smul_iff, Subgroup.exists_leftTransversal_of_FiniteIndex, mem_balancedHull_iff, smul_unitBall_of_pos, gauge_smul_left_of_nonneg, UniqueDiffWithinAt.smul_iff, Bornology.IsBounded.smulβ, op_smul_set_mul_eq_mul_smul_set, Metric.smul_sphere, iUnion_inv_smul, op_smul_inter_nonempty_iff, IsClosed.leftCoset, natCard_smul_set, Finset.coe_smul_finset, StarConvex.smul, isFoelner_iff, MeasureTheory.measure_smul_null, amenable_of_maxFoelner_neBot, LinearOrderedField.smul_Ioo, IsFoelner.tendsto_meas_smul_symmDiff_smul, MeasureTheory.IsFundamentalDomain.setLIntegral_eq_tsum', AddSubmonoid.smul_closure, zero_smul_set, Balanced.smul, inv_smul_set_distribβ, smul_closure_orbit_subset, Convex.combo_closure_interior_subset_interior, Bornology.IsBounded.smul, smul_mem_nhds_smul_iffβ, Convex.add_smul, gauge_def, Subgroup.IsComplement.pairwiseDisjoint_smul, MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum, preimage_smul, infDist_smulβ, smulCommClass_set, MapsTo.smul_set, smul_set_union, derivWithin_comp_mul_left, iUnion_smul_set, QuotientGroup.orbit_eq_out_smul, preimage_smul_inv, Submodule.smul_closure_subset, MulAction.IsBlock.smul_eq_smul_or_disjoint, IsOpen.dense_iUnion_smul, mem_inv_smul_set_iff, IsLowerSet.smul_subset, smul_set_iInter, ediam_smul, smul_set_compl, Cardinal.mk_smul_setβ, MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one, absorbs_iff_norm, MeasureTheory.IsFundamentalDomain.smul, smul_set_sdiff, smulCommClass_set', smul_closedBall'', diam_smul, Nonempty.smul_set, smul_pi, MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac, MapsTo.smul_setββ, smul_set_pi_of_isUnit, smul_mem_nhds_smul, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset', neg_smul_set, inv_smul_set_distrib, IsOpen.rightCoset, PrimeSpectrum.zeroLocus_smul_of_isUnit, Subgroup.smul_closure, smul_upperBounds_subset_lowerBounds_smul, StrictConvex.smul, MulAction.IsBlock.isBlockSystem, IsOpen.smul, MeasurableSet.const_smulβ, smul_unitBall, rightCoset_mem_rightCoset, smul_mem_nhds_smul_iff, isScalarTower, ZLattice.covolume.tendsto_card_div_pow', iUnion_smul_eq_setOf_exists, DiscreteTiling.PlacedTile.coe_smul, MulAction.coe_aestabilizer, MeasureTheory.IsFundamentalDomain.measure_eq_tsum', IsUnit.preimage_smul_set, iUnion_op_smul_set, MeasureTheory.smul_mem_ae, IsFoelner.mean_smul_eq_mean, leftCoset_mem_leftCoset, MulAction.isBlock_iff_smul_eq_smul_or_disjoint, MeasureTheory.measure_inv_smul_symmDiff, hasDerivWithinAt_comp_mul_left_smul_iff, Algebra.pow_smul_mem_adjoin_smul, MeasureTheory.Measure.addHaar_smul_of_nonneg, Metric.smul_closedBall, Metric.smul_eball, MulAction.isBlock_iff_disjoint_smul_of_ne, smul_set_sdiffβ, MeasurableSet.const_smul_of_ne_zero, MulAction.mem_stabilizer_set_iff_smul_set_subset, smul_set_univ, support_comp_inv_smul, smul_set_singleton, mul_pair, Seminorm.smul_closedBall_subset, Submodule.span_smul, smul_set_range, IsUpperSet.smul, lowerBounds_smul_of_neg, MulAction.smul_fixedBy, exists_lt_of_gauge_lt, MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul, MeasureTheory.measure_smul, Subsemiring.coe_pointwise_smul, MeasureTheory.NullMeasurableSet.smul, MeasureTheory.measure_inv_smul_union, smul_set_eq_univ, mul_subset_iff_right, mem_own_leftCoset, isSimplyConnected_smul_setβ_iff, MeasureTheory.eventually_nhds_one_measure_smul_diff_lt, smul_lowerBounds_subset_lowerBounds_smul_of_nonneg, egauge_eq_zero_iff, mul_subset_iff_left, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset, Group.preimage_smul_set, MeasureTheory.IsFundamentalDomain.integral_eq_tsum_of_ac, MeasureTheory.Measure.setIntegral_comp_smul, ValuationSubring.coe_pointwise_smul, ediam_smulβ, MeasureTheory.Measure.addHaar_nnreal_smul, Absorbs.exists_pos, MulAction.IsTopologicallyTransitive.exists_smul_inter, MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul, smul_set_nonempty, MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac, MeasureTheory.IsFundamentalDomain.aedisjoint, MulAction.IsBlock.translate, smul_inter_nonempty_iff, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq, orbit_subgroup_eq_rightCoset, smul_set_univ_pi, gauge_lt_eq', MeasureTheory.measure_inv_smul_inter, LinearOrderedField.smul_Ici, encard_smul_set, smul_univ_pi, IsOpen.smulβ, ConvexBody.iInter_smul_eq_self, smul_lowerBounds_subset_upperBounds_smul, convex_iff_pointwise_add_subset, inv_op_smul_set_distrib, Finite.smul_set, MeasureTheory.smul_set_ae_eq, smul_div_smul_comm, op_smul_set_subset_mul, MulAction.isTopologicallyTransitive_iff_dense_iUnion, Real.sInf_smul_of_nonpos, LinearOrderedField.smul_Ioi, BddAbove.smul_of_nonpos, smul_ball, Submonoid.smul_closure, threeGPFree_smul_set, MeasureTheory.distribHaarChar_eq_div, smul_inter_nonempty_iff', AddSubgroup.coe_pointwise_smul, MulAction.IsBlock.pairwiseDisjoint_range_smul, MulAction.isBlock_iff_pairwiseDisjoint_range_smul, smul_set_iUnion, AddSubmonoid.coe_pointwise_smul, mem_leftCoset, MulAction.IsBlock.not_smul_set_ssubset_smul_set, MeasureTheory.hausdorffMeasure_smul, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range, MeasureTheory.distribHaarChar_mul, LinearOrderedField.smul_Ioc, MulAction.isBlock_iff_smul_eq_of_nonempty, smul_set_eq_empty, image_op_smul_distrib, ConvexCone.mem_hull_of_convex, QuotientGroup.orbit_mk_eq_smul, preimage_smulβ, smul_set_prod, zero_mem_smul_set, eq_cosets_of_normal, MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux, range_smul, SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter, MeasurableSet.const_smul, Submodule.smul_span, Finset.op_smul_stabilizer_of_no_doubling, smul_piβ, pairwise_disjoint_smul_iff, bddBelow_smul_iff_of_pos, convexHull_smul, smul_mem_smul_set_iff, totallyBounded_iff_subset_finite_iUnion_nhds_one, mem_smul_set_iff_inv_smul_mem, smul_Icc, smul_set_subset_smul_set_iff, lowerClosure_smul, Infinite.smul_set, range_mul, DiscreteTiling.PlacedTile.coe_mk_coe, Seminorm.smul_ball_zero, MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed, bddAbove_smul_iff_of_pos, LinearOrderedField.smul_Iic, ThreeGPFree.smul_set, egauge_eq_top, gauge_smul_left, pairwiseDisjoint_smul_iff, MulAction.IsBlock.smul_eq_or_disjoint, MeasureTheory.Measure.setIntegral_comp_smul_of_pos, ConvexCone.coe_hull_of_convex, smulCommClass_set'', Group.preimage_smul_setββ, smul_preimage_set_subsetββ, Submonoid.pow_smul_mem_closure_smul, preimage_smul_setββ', spectrum.unit_smul_eq_smul, MeasureTheory.smul_set_ae_le, LinearOrderedField.smul_Icc, Subsemiring.smul_closure, rightCoset_one, disjoint_smul_set_left, Monoid.CoprodI.lift_word_ping_pong, smul_set_subset_iffβ, smul_ball_one, spectrum.smul_eq_smul, disjoint_smul_set_right, MeasureTheory.fundamentalInterior_smul, IsCompact.smul, gauge_lt_eq, Submodule.mem_div_iff_smul_subset, toFinset_smul_set, Balanced.smul_eq, exists_disjoint_smul_of_isCompact, smul_closedBall, leftCoset_rightCoset, EMetric.smul_closedBall, add_smul_subset, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset, smul_set_sInter_subset, Filter.smul_set_mem_smul_filter, GrpCat.SurjectiveOfEpiAuxs.Ο_symm_apply_fromCoset, mem_rightCoset_iff, ZLattice.covolume.tendsto_card_div_pow'', IsFoelner.amenable, MeasureTheory.measure_union_inv_smul, smul_set_subset_iff_subset_inv_smul_set, closure_smul, fderivWithin_comp_smul, BddBelow.smul_of_nonneg, smul_set_piβ', MulAction.isTopologicallyTransitive_iff, mulSupport_comp_inv_smulβ, egauge_lt_iff, threeGPFree_smul_setβ, iUnion_smul_left_image, MulAction.IsTrivialBlock.smul_iff, mem_smul_set_iff_inv_smul_memβ, smul_graphOn, MulAction.smul_zpow_fixedBy_eq_of_commute, approxOrderOf.smul_eq_of_mul_dvd, Flag.coe_smul, rightCoset_assoc, QuotientGroup.sound, image_smul_comm, bddAbove_smul_iff_of_neg, MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq, smul_set_symmDiffβ, IsUnit.preimage_smul_setββ, zero_smul_set_subset, MeasureTheory.IsFundamentalDomain.smul_of_comm, Convex.mem_smul_of_zero_mem, balancedCore_eq_iInter, Metric.infEDist_smul, MeasureTheory.IsFundamentalDomain.measure_eq_tsum, StrictConvex.mem_smul_of_zero_mem, GrpCat.SurjectiveOfEpiAuxs.Ο_apply_fromCoset', ConvexBody.coe_smul', upperBounds_smul_of_pos, upperClosure_smul, MulAction.IsBlock.smul_eq_of_mem, Finset.smul_stabilizer_of_no_doubling, smul_set_piβ, Balanced.smul_mono, IsUpperSet.smul_subset, MeasureTheory.IsFundamentalDomain.integral_eq_tsum, smul_mem_smul_set, inv_op_smul_set_distribβ, smul_set_subset_iff, SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter, subset_smul_set_iffβ, MulAction.smul_orbit_eq_orbit_smul, IsClosed.rightCoset, smul_pi_subset, egauge_smul_left, MeasureTheory.Measure.addHaar_smul, StarConvex.mem_smul, AffineSubspace.smul_span, IsClosed.smul, isScalarTower', smul_closure_subset
|
vadd π | CompOp | 70 mathmath: iUnion_vadd, HahnModule.support_smul_subset_vadd_support', IsOpen.vadd_left, vadd_singleton, vadd_mem_vadd, Filter.mem_vadd, vadd_set_subset_vadd, IsPWO.vadd, vadd_subset_iff, vadd_subset_vadd, vadd_inter_subset, Finset.support_vaddAntidiagonal_subset_vadd, set_vadd_closure_subset, sInter_vadd_subset, vadd_nonempty, iInterβ_vadd_subset, IsCompact.vadd_set, Filter.vadd_mem_vadd, inter_vadd_union_subset_union, IsClosed.vadd_right_of_isCompact, Nonempty.vadd, vadd_singleton_mem_nhds_of_sigmaCompact, image_op_vadd, vadd_iInterβ_subset, mem_vadd, union_vadd_inter_subset_union, image2_vadd, vadd_iInter_subset, vadd_univ, vaddCommClass, vadd_iUnionβ, IsClosed.vadd_left_of_isCompact, Finset.coe_vadd, sUnion_vadd, vadd_set_closure_subset, singleton_vadd, vadd_union, range_vadd_range, inter_vadd_subset, Filter.HasBasis.vadd, vadd_sUnion, empty_vadd, vadd_image_prod, vaddAssocClass'', iUnion_vadd_right_image, vaddCommClass_set'', op_vadd_set_vadd_eq_vadd_vadd_set, Filter.le_vadd_iff, subset_interior_vadd, vaddCommClass_set', HahnModule.support_smul_subset_vadd_support, vadd_iUnion, vadd_subset_vadd_right, toFinset_vadd, iUnionβ_vadd, union_vadd, Finite.toFinset_vadd, vadd_eq_empty, vaddAssocClass', iUnion_vadd_set, IsWF.min_vadd, vadd_sInter_subset, Finite.vadd, singleton_vadd_singleton, IsWF.vadd, subset_interior_vadd_right, vadd_empty, iUnion_vadd_left_image, vadd_subset_vadd_left, iInter_vadd_subset
|
vaddSet π | CompOp | 343 mathmath: ncard_vadd_set, AddAction.mem_stabilizer_set_iff_subset_vadd_set, ball_sub, Metric.infEDist_vadd, Metric.vadd_closedBall, vadd_set_pi_of_surjective, AddAction.IsTrivialBlock.vadd_iff, vadd_set_iUnionβ, fderivWithin_comp_add_left, rank_le_card_isVisible, MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum, vadd_set_subset_vadd, IsUpperSet.vadd, vadd_set_inter_subset, rightAddCoset_zero, Convex.vadd, image_vadd_setββ, vadd_eq_self_of_preimage_zsmul_eq_self, AddAction.isTopologicallyTransitive_iff, rightAddCoset_mem_rightAddCoset, AddAction.IsBlock.ncard_block_add_ncard_orbit_eq, QuotientAddGroup.univ_eq_iUnion_vadd, Dense.vadd, MeasureTheory.IsAddFundamentalDomain.sum_restrict, derivWithin_comp_const_sub, iUnion_neg_vadd, vadd_mem_vadd_set, mem_vadd_set, iteratedFDerivWithin_comp_add_right', Finset.coe_vadd_finset, AddAction.Supports.vadd, approxAddOrderOf.vadd_eq_of_mul_dvd, vadd_set_compl, MeasureTheory.mem_addFundamentalFrontier, EMetric.vadd_ball, IsLowerSet.vadd_subset, op_vadd_set_add_eq_add_vadd_set, threeAPFree_vadd_set, isLinearSet_iff, MeasureTheory.measure_neg_vadd_inter, MapsTo.vadd_set, IsOpen.left_addCoset, AddSubmonoid.nsmul_vadd_mem_closure_vadd, AddAction.IsBlock.translate, vadd_set_vsub_vadd_set, exists_disjoint_vadd_of_isCompact, vadd_set_sdiff, Finset.op_vadd_stabilizer_of_no_doubling, MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq, op_vadd_set_subset_add, vadd_set_univ_pi, IsLowerSet.vadd, AddAction.isPreprimitive_ofFixingAddSubgroup_conj_iff, mem_rightAddCoset, vadd_set_pi_of_isAddUnit, IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd, OrdConnected.vadd, AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty, IsAddUnit.preimage_vadd_setββ, MeasureTheory.IsAddFundamentalDomain.restrict_restrict, neg_op_vadd_set_distrib, iteratedFDerivWithin_comp_add_left, vadd_sub_vadd_comm, pairwise_disjoint_vadd_iff, AddAction.isBlock_iff_vadd_eq_of_nonempty, MeasureTheory.IsAddFundamentalDomain.vadd_of_comm, affinity_unitClosedBall, MeasureTheory.measure_vadd, vadd_set_insert, vadd_set_eq_empty, AddAction.IsTopologicallyTransitive.exists_vadd_inter, Metric.vadd_ball, vadd_set_range, MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet_vadd, add_subset_iff_left, vadd_mem_vadd_set_iff, vadd_Icc, IsAddFoelner.mean_vadd_eq_mean_vadd, AddAction.IsBlock.vadd_eq_vadd_or_disjoint, toFinset_vadd_set, IsSemilinearSet.vadd, convexHull_vadd, EMetric.infEdist_vadd, NonarchimedeanAddGroup.exists_openAddSubgroup_separating, MeasureTheory.vadd_set_ae_le, IsCompact.exists_finite_cover_vadd, MeasureTheory.measure_sdiff_neg_vadd, AddAction.vadd_fixedBy, MeasureTheory.measure_neg_vadd_symmDiff, AffineSubspace.coe_pointwise_vadd, Finite.toFinset_vadd_set, vadd_set_singleton, AddAction.IsBlock.pairwiseDisjoint_range_vadd, IsAddUnit.preimage_vadd_set, image_vadd, IsUpperSet.vadd_subset, MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum, MeasureTheory.tendsto_measure_vadd_diff_isCompact_isClosed, AddGroup.preimage_vadd_set, op_vadd_coe_set, vadd_graphOn_univ, affinity_unitBall, isSimplyConnected_vadd_set_iff, vadd_set_eq_univ, AmpleSet.vadd, AddAction.IsTrivialBlock.vadd, vadd_set_subset_vadd_set_iff, Metric.vadd_sphere, StrictConvex.affinity, MeasureTheory.mem_addFundamentalInterior, iteratedFDerivWithin_comp_sub, image_vadd_distrib, differentiableWithinAt_comp_sub, vadd_ball_zero, vadd_preimage_set_subset, MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum', MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq, MeasureTheory.IsAddFundamentalDomain.pairwise_aedisjoint_of_ac, vadd_inter_nonempty_iff', IsClosed.vadd, preimage_vadd_neg, MeasureTheory.measure_vadd_eq_zero_iff, interior_vadd, mem_leftAddCoset_iff, MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum, mem_rightAddCoset_iff, AddAction.vadd_orbit_eq_orbit_vadd, QuotientAddGroup.sound, AddAction.IsBlock.not_vadd_set_ssubset_vadd_set, isProperLinearSet_iff, vadd_set_prod, AddAction.vadd_orbit, iUnion_op_vadd_set, AddGroup.preimage_vadd_setββ, vaddAssocClass, SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj, MeasureTheory.measure_neg_vadd_sdiff, Seminorm.vadd_closedBall, vadd_set_univ, vadd_set_sUnion, vadd_closedBall'', mem_own_leftAddCoset, AddAction.vadd_orbit_subset, add_pair, AddAction.IsBlock.isBlockSystem, AddAction.IsBlock.of_subset, vadd_segment, AddAction.isBlock_iff_vadd_eq_or_disjoint, MeasureTheory.vadd_mem_ae, image_vadd_set, iteratedFDerivWithin_comp_add_right, vadd_mem_nhds_vadd, AddAction.IsBlock.of_addSubgroup_of_conjugate, AddAction.coe_aestabilizer, vadd_set_subset_iff_subset_neg_vadd_set, AddAction.IsPreprimitive.exists_mem_vadd_and_notMem_vadd, AmpleSet.vadd_iff, IsOpen.iUnion_vadd, exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add, vadd_mem_nhds_self, singleton_vadd, AddAction.IsBlock.disjoint_vadd_of_ne, vadd_set_subset_iff, differentiableWithinAt_comp_add_right, vadd_graphOn, AddSubgroup.leftCoset_cover_const_iff_surjOn, rightAddCoset_eq_iff, AddAction.vadd_zsmul_movedBy_eq_of_addCommute, range_vadd, preimage_vadd_setββ', MeasureTheory.hausdorffMeasure_vadd, range_add, ediam_vadd, infinite_vadd_set, AddAction.op_vadd_set_stabilizer_subset, leftAddCoset_eq_iff, eq_addCosets_of_normal, vadd_set_subset_add, MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt, MeasureTheory.vadd_set_ae_eq, MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum_of_ac, AddMonoidHom.preimage_vadd_setββ, Metric.vadd_closedEBall, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum, vadd_closure_subset, natCard_vadd_set, AddAction.isBlock_iff_disjoint_vadd_of_ne, preimage_vadd_setββ_of_isAddUnit_isAddUnit, AddAction.vadd_zsmul_fixedBy_eq_of_addCommute, op_vadd_inter_nonempty_iff, AddAction.isBlock_iff_pairwiseDisjoint_range_vadd, vectorSpan_vadd, Bornology.IsVonNBounded.vadd, vadd_openSegment, image_vadd_comm, IsLinearSet.vadd, AddSubgroup.IsComplement.pairwiseDisjoint_vadd, disjoint_vadd_set, ball_add, lowerClosure_vadd, IsCompact.sub_closedBall, AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint, MeasureTheory.IsAddFundamentalDomain.setLIntegral_eq_tsum, vadd_set_iUnion, mem_leftAddCoset, EMetric.vadd_closedBall, add_ball, vadd_univ_pi, hasFDerivWithinAt_comp_add_right, MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac, isLinearSet_iff_exists_fg_eq_vadd, Infinite.vadd_set, AddAction.isTopologicallyTransitive_iff_dense_iUnion, Cardinal.mk_vadd_set, vadd_set_mono, leftAddCoset_rightAddCoset, QuotientAddGroup.orbit_eq_out_vadd, vadd_set_empty, iteratedFDerivWithin_comp_add_left', mem_vadd_set_neg, MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum_of_ac, vadd_pi_subset, MeasureTheory.measure_inter_neg_vadd, mem_own_rightAddCoset, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum', vaddCommClass_set'', MeasureTheory.measure_union_neg_vadd, vadd_closedBall_zero, vaddCommClass_set, diam_vadd, disjoint_vadd_set_left, vadd_set_nonempty, op_vadd_set_vadd_eq_vadd_vadd_set, vadd_closure_orbit_subset, vadd_coe_set, Nonempty.vadd_set, pairwiseDisjoint_vadd_iff, MeasureTheory.IsAddFundamentalDomain.vadd, upperClosure_vadd, IsAddFoelner.mean_vadd_eq_mean, add_subset_iff_right, derivWithin_comp_add_const, Bornology.isVonNBounded_vadd, Ideal.univ_eq_iUnion_image_add, neg_vadd_set_distrib, MeasureTheory.measure_symmDiff_neg_vadd, vaddCommClass_set', IsCompact.vadd, rightAddCoset_assoc, support_translate, mem_neg_vadd_set_iff, amenable_of_maxAddFoelner_neBot, Finset.vadd_stabilizer_of_no_doubling, Seminorm.vadd_ball, IsAddFoelner.tendsto_meas_vadd_symmDiff, zero_leftAddCoset, disjoint_vadd_set_right, Metric.vadd_eball, AddAction.mem_stabilizer_set_iff_vadd_set_subset, hasFDerivWithinAt_comp_sub, derivWithin_comp_sub_const, vadd_preimage_set_subsetββ, vadd_set_symmDiff, vaddAssocClass', IsCompact.closedBall_add, Finite.vadd_set, WithIdealFilter.mem_nhds_iff, QuotientAddGroup.eq_class_eq_leftCoset, iUnion_vadd_set, MeasureTheory.measure_neg_vadd_union, preimage_vadd, AddSubgroup.exists_leftTransversal_of_FiniteIndex, MeasureTheory.IsAddFundamentalDomain.aedisjoint, MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd, orbit_addSubgroup_eq_rightCoset, vadd_set_union, vadd_mem_nhds_vadd_iff, differentiableWithinAt_comp_add_left, normal_iff_eq_addCosets, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac, MeasureTheory.addFundamentalFrontier_vadd, vadd_set_iInter, AddAction.mem_aestabilizer, MeasureTheory.pairwise_disjoint_addFundamentalInterior, derivWithin_comp_const_add, AffineSubspace.pointwise_vadd_span, convex_vadd, vadd_inter_nonempty_iff, iUnion_vadd_eq_setOf_exists, ThreeAPFree.vadd_set, AddAction.le_stabilizer_iff_vadd_le, MeasureTheory.addFundamentalInterior_vadd, iteratedFDerivWithin_comp_sub', IsOpen.right_addCoset, MeasureTheory.IsAddFundamentalDomain.setIntegral_eq_tsum', MeasureTheory.eventuallyConst_vadd_set_ae, vadd_ball'', fderivWithin_comp_add_right, vadd_set_inter, IsOpen.vadd, MapsTo.vadd_setββ, subset_vadd_set_iff, MeasureTheory.measure_vadd_null, IsClosed.right_addCoset, IsClosed.left_addCoset, approxAddOrderOf.vadd_subset_of_coprime, Absorbent.vadd_absorbs, StrictConvex.vadd, iUnion_vadd_left_image, mem_vadd_set_iff_neg_vadd_mem, vadd_set_iInterβ_subset, sub_ball, vadd_pi, IsAddFoelner.amenable, totallyBounded_iff_subset_finite_iUnion_nhds_zero, leftAddCoset_mem_leftAddCoset, IsOpen.dense_iUnion_vadd, isCentralVAdd, spectrum.vadd_eq, AddAction.IsBlock.vadd_eq_of_mem, isAddFoelner_iff, Bornology.IsBounded.vadd, leftAddCoset_assoc, MeasureTheory.NullMeasurableSet.vadd, vadd_set_sInter_subset, AddAction.isBlock_iff_vadd_eq_of_mem, fderivWithin_comp_sub, Filter.vadd_set_mem_vadd_filter, IsCompact.add_closedBall, AddAction.vadd_set_stabilizer_subset, finite_vadd_set, AddAction.IsBlock.vadd_eq_or_disjoint, QuotientAddGroup.orbit_mk_eq_vadd, closure_vadd, hasFDerivWithinAt_comp_add_left, vadd_set_pi, MeasurableSet.const_vadd, image_op_vadd_distrib, encard_vadd_set, isLinearSet_iff_exists_fin_addMonoidHom, vadd_set_iInter_subset, IsCompact.closedBall_sub, pair_add
|
vsub π | CompOp | 50 mathmath: vsub_subset_vsub_right, Finite.toFinset_vsub, vsub_subset_vsub_left, vsub_singleton, iUnion_vsub_left_image, vsub_nonempty, vadd_set_vsub_vadd_set, Finite.vsub, sUnion_vsub, Filter.le_vsub_iff, inter_vsub_subset, mem_vsub, vsub_sUnion, Filter.mem_vsub, AffineSubspace.coe_direction_eq_vsub_set, vsub_iInterβ_subset, toFinset_vsub, vsub_subset_iff, inter_vsub_union_subset_union, vsub_iUnion, singleton_vsub_singleton, vsub_iInter_subset, sInter_vsub_subset, vsub_eq_empty, Nonempty.vsub, empty_vsub, union_vsub, union_vsub_inter_subset_union, vsub_self_mono, singleton_vsub, iUnion_vsub, iInterβ_vsub_subset, vsub_mem_vsub, vsub_empty, vectorSpan_def, image_vsub_prod, vsub_union, iUnion_vsub_right_image, image2_vsub, iUnionβ_vsub, vsub_inter_subset, vsub_sInter_subset, vsub_iUnionβ, iInter_vsub_subset, vsub_subset_vsub, vsub_set_subset_vectorSpan, AffineMap.image_vsub_image, Finset.coe_vsub, Filter.vsub_mem_vsub, singleton_vsub_self
|