CovBySMul

📁 Source: Mathlib/Combinatorics/Additive/CovBySMul.lean

Statistics

Metric	Count
Definitions CovBySMul, CovByVAdd	2
Theorems mono, nonneg, of_subset, rfl, subset, subset_left, subset_right, trans, mono, nonneg, of_subset, rfl, subset, subset_left, subset_right, trans, covBySMul_zero, covByVAdd_zero	18
Total	20

CovBySMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Real Real.instLE CovBySMul	—	—	LE.le.trans
nonneg 📖	mathematical	CovBySMul	Real Real.instLE Real.instZero	—	LE.le.trans Nat.cast_nonneg Real.instIsOrderedRing
of_subset 📖	mathematical	Set Set.instHasSubset	CovBySMul Real Real.instOne	—	Finset.card_one Nat.cast_one Finset.coe_one one_smul
rfl 📖	mathematical	—	CovBySMul Real Real.instOne	—	Finset.card_one Nat.cast_one Finset.coe_one one_smul Set.instReflSubset
subset 📖	—	Set Set.instHasSubset CovBySMul	—	—	subset_right subset_left
subset_left 📖	—	Set Set.instHasSubset CovBySMul	—	—	one_mul trans IsScalarTower.left of_subset
subset_right 📖	—	Set Set.instHasSubset CovBySMul	—	—	mul_one trans IsScalarTower.left of_subset
trans 📖	mathematical	CovBySMul	Real Real.instMul	—	nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.card_smul_le mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Nat.cast_nonneg' Set.smul_subset_smul subset_refl Set.instReflSubset Finset.coe_smul smul_assoc Set.isScalarTower''

CovByVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Real Real.instLE CovByVAdd	—	—	LE.le.trans
nonneg 📖	mathematical	CovByVAdd	Real Real.instLE Real.instZero	—	LE.le.trans Nat.cast_nonneg Real.instIsOrderedRing
of_subset 📖	mathematical	Set Set.instHasSubset	CovByVAdd Real Real.instOne	—	Finset.card_zero Nat.cast_one le_refl Finset.coe_zero zero_vadd
rfl 📖	mathematical	—	CovByVAdd Real Real.instOne	—	Finset.card_zero Nat.cast_one le_refl Finset.coe_zero zero_vadd subset_refl Set.instReflSubset
subset 📖	—	Set Set.instHasSubset CovByVAdd	—	—	subset_right subset_left
subset_left 📖	—	Set Set.instHasSubset CovByVAdd	—	—	one_mul trans VAddAssocClass.left of_subset
subset_right 📖	—	Set Set.instHasSubset CovByVAdd	—	—	mul_one trans VAddAssocClass.left of_subset
trans 📖	mathematical	CovByVAdd	Real Real.instMul	—	nonneg Nat.cast_mul Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.card_vadd_le mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Nat.cast_nonneg' Set.vadd_subset_vadd subset_refl Set.instReflSubset Finset.coe_vadd vadd_assoc Set.vaddAssocClass''

(root)

Definitions

Name	Category	Theorems
CovBySMul 📖	MathDef	5 math math: covBySMul_zero, CovBySMul.rfl, IsApproximateSubgroup.sq_covBySMul, IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq, CovBySMul.of_subset
CovByVAdd 📖	MathDef	5 math math: covByVAdd_zero, CovByVAdd.of_subset, IsApproximateAddSubgroup.two_nsmul_covByVAdd, CovByVAdd.rfl, IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covBySMul_zero 📖	mathematical	—	CovBySMul Real Real.instZero Set Set.instEmptyCollection	—	IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.coe_empty Set.empty_smul
covByVAdd_zero 📖	mathematical	—	CovByVAdd Real Real.instZero Set Set.instEmptyCollection	—	Nat.cast_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.card_eq_zero Finset.coe_empty Set.empty_vadd Set.subset_empty_iff

---

← Back to Index