Defs

📁 Source: Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean

Statistics

Metric	Count
Definitions IsLinearSet, IsProperLinearSet, IsProperSemilinearSet, IsSemilinearSet	4
Theorems add, closure, closure_finset, closure_of_finite, image, isProperSemilinearSet, isSemilinearSet, of_fg, singleton, univ, vadd, isLinearSet, isProperSemilinearSet, singleton, biUnion, biUnion_finset, empty, isSemilinearSet, sUnion, union, add, biUnion, biUnion_finset, closure, closure_finset, closure_of_finite, empty, iUnion, image, isProperSemilinearSet, of_fg, of_finite, proj, proj', sUnion, singleton, union, univ, vadd, isSemilinearSet_iff_ultimately_periodic, isLinearSet_iff, isLinearSet_iff_exists_fg_eq_vadd, isProperLinearSet_iff, isProperSemilinearSet_iff, isSemilinearSet_iff, isSemilinearSet_image_iff	46
Total	50

IsLinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsLinearSet	IsLinearSet Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.Finite.union vadd_add_vadd Set.vaddAssocClass' VAddAssocClass.left Set.vaddAssocClass Set.vaddCommClass_set' vaddCommClass_self AddSubmonoid.closure_union AddSubmonoid.coe_sup
closure 📖	mathematical	IsLinearSet	IsSemilinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	Set.ext AddSubmonoid.closure_induction AddSubmonoid.closure_mono Set.subset_insert zero_add add_zero AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass AddSubmonoid.mem_closure_of_mem Set.mem_insert add_right_comm AddSubmonoidClass.toZeroMemClass AddSubmonoid.closure_union add_left_comm nsmul_mem Set.vadd_mem_vadd_set ZeroMemClass.zero_mem IsSemilinearSet.union IsSemilinearSet.singleton isSemilinearSet
closure_finset 📖	mathematical	—	IsLinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure Finset Finset.instSetLike	—	zero_vadd
closure_of_finite 📖	mathematical	—	IsLinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	zero_vadd
image 📖	mathematical	IsLinearSet	IsLinearSet Set.image DFunLike.coe	—	Set.Finite.image Set.image_vadd_distrib AddMonoidHomClass.toAddHomClass
isProperSemilinearSet 📖	mathematical	IsLinearSet	IsProperSemilinearSet	—	isLinearSet_iff Nat.strong_induction_on IsProperLinearSet.isProperSemilinearSet not_linearIndepOn_finset_iffₒₛ Nat.instCanonicallyOrderedAdd IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Set.ext AddSubmonoid.mem_closure_finset Finset.union_sdiff_of_subset IsCancelAdd.toIsLeftCancelAdd Finset.sum_union Disjoint.symm Finset.sdiff_disjoint Finset.sum_congr ite_smul Finset.sum_ite Finset.filter_mem_eq_inter Finset.inter_eq_right Finset.filter_notMem_eq_sdiff add_smul Finset.sum_add_distrib add_right_comm tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instOrderedSub Mathlib.Tactic.Push.not_forall_eq Set.iUnion_congr_Prop sum_mem AddSubmonoid.instAddSubmonoidClass nsmul_mem AddSubmonoid.mem_closure_of_mem Finset.sum_erase_add add_assoc AddMemClass.add_mem AddSubmonoidClass.toAddMemClass AddSubmonoid.closure_mono Finset.erase_subset IsProperSemilinearSet.biUnion_finset Finset.card_lt_card Finset.erase_ssubset
isSemilinearSet 📖	mathematical	IsLinearSet	IsSemilinearSet	—	Set.sUnion_singleton
of_fg 📖	mathematical	AddSubmonoid.FG AddCommMonoid.toAddMonoid	IsLinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike	—	isLinearSet_iff_exists_fg_eq_vadd zero_vadd
singleton 📖	mathematical	—	IsLinearSet Set Set.instSingletonSet	—	AddSubmonoid.closure_empty Set.vadd_set_singleton add_zero
univ 📖	mathematical	—	IsLinearSet Set.univ	—	of_fg AddMonoid.FG.fg_top
vadd 📖	mathematical	IsLinearSet	IsLinearSet HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	vadd_vadd

IsProperLinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLinearSet 📖	mathematical	IsProperLinearSet	IsLinearSet	—	—
isProperSemilinearSet 📖	mathematical	IsProperLinearSet	IsProperSemilinearSet	—	Set.sUnion_singleton
singleton 📖	mathematical	—	IsProperLinearSet Set Set.instSingletonSet	—	AddSubmonoid.closure_empty Set.vadd_set_singleton add_zero

IsProperSemilinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion 📖	mathematical	IsProperSemilinearSet	IsProperSemilinearSet Set.iUnion Set Set.instMembership	—	Set.sUnion_image sUnion Set.Finite.image
biUnion_finset 📖	mathematical	IsProperSemilinearSet	IsProperSemilinearSet Set.iUnion Finset SetLike.instMembership Finset.instSetLike	—	biUnion Finset.finite_toSet
empty 📖	mathematical	—	IsProperSemilinearSet Set Set.instEmptyCollection	—	instIsEmptyFalse Set.sUnion_empty
isSemilinearSet 📖	mathematical	IsProperSemilinearSet	IsSemilinearSet	—	IsProperLinearSet.isLinearSet
sUnion 📖	mathematical	IsProperSemilinearSet	IsProperSemilinearSet Set.sUnion	—	Set.Finite.induction_on Set.sUnion_empty Set.sUnion_insert union
union 📖	mathematical	IsProperSemilinearSet	IsProperSemilinearSet Set Set.instUnion	—	Set.sUnion_union Set.Finite.union Set.mem_union

IsSemilinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.sUnion_add Set.iUnion_congr_Prop Set.add_sUnion biUnion IsLinearSet.isSemilinearSet IsLinearSet.add
biUnion 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set.iUnion Set Set.instMembership	—	Set.sUnion_image sUnion Set.Finite.image
biUnion_finset 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set.iUnion Finset SetLike.instMembership Finset.instSetLike	—	biUnion Finset.finite_toSet
closure 📖	mathematical	IsSemilinearSet	IsSemilinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	Set.Finite.induction_on Set.sUnion_empty AddSubmonoid.closure_empty Set.sUnion_insert AddSubmonoid.closure_union AddSubmonoid.coe_sup add IsLinearSet.closure
closure_finset 📖	mathematical	—	IsSemilinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure Finset Finset.instSetLike	—	IsLinearSet.isSemilinearSet IsLinearSet.closure_finset
closure_of_finite 📖	mathematical	—	IsSemilinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike AddSubmonoid.closure	—	IsLinearSet.isSemilinearSet IsLinearSet.closure_of_finite
empty 📖	mathematical	—	IsSemilinearSet Set Set.instEmptyCollection	—	instIsEmptyFalse Set.sUnion_empty
iUnion 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set.iUnion	—	Set.sUnion_range sUnion Set.finite_range
image 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set.image DFunLike.coe	—	Set.sUnion_eq_biUnion Set.image_iUnion biUnion IsLinearSet.isSemilinearSet IsLinearSet.image
isProperSemilinearSet 📖	mathematical	IsSemilinearSet	IsProperSemilinearSet	—	Set.sUnion_eq_biUnion IsProperSemilinearSet.biUnion IsLinearSet.isProperSemilinearSet
of_fg 📖	mathematical	AddSubmonoid.FG AddCommMonoid.toAddMonoid	IsSemilinearSet SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike	—	IsLinearSet.isSemilinearSet IsLinearSet.of_fg
of_finite 📖	mathematical	—	IsSemilinearSet	—	Set.biUnion_of_singleton biUnion
proj 📖	mathematical	IsSemilinearSet Pi.addCommMonoid	IsSemilinearSet Pi.addCommMonoid setOf Set Set.instMembership	—	Set.ext image DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
proj' 📖	mathematical	IsSemilinearSet Pi.addCommMonoid setOf	IsSemilinearSet Pi.addCommMonoid setOf	—	proj
sUnion 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set.sUnion	—	Set.Finite.induction_on Set.sUnion_empty Set.sUnion_insert union
singleton 📖	mathematical	—	IsSemilinearSet Set Set.instSingletonSet	—	IsLinearSet.isSemilinearSet IsLinearSet.singleton
union 📖	mathematical	IsSemilinearSet	IsSemilinearSet Set Set.instUnion	—	Set.sUnion_union Set.Finite.union Set.mem_union
univ 📖	mathematical	—	IsSemilinearSet Set.univ	—	IsLinearSet.isSemilinearSet IsLinearSet.univ
vadd 📖	mathematical	IsSemilinearSet	IsSemilinearSet HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	Set.vadd_set_sUnion biUnion IsLinearSet.isSemilinearSet IsLinearSet.vadd

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSemilinearSet_iff_ultimately_periodic 📖	mathematical	—	IsSemilinearSet instAddCommMonoid Set Set.instMembership	—	isProperSemilinearSet_iff IsSemilinearSet.isProperSemilinearSet IsOrderedCancelAddMonoid.toIsCancelAdd instIsOrderedCancelAddMonoid isProperLinearSet_iff Cardinal.mk_fintype Fintype.card_coe CommSemiring.rank_self Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero LinearIndependent.cardinal_le_rank instNontrivial zero_lt_one instZeroLEOneClass Finset.coe_empty AddSubmonoid.closure_empty Set.vadd_set_singleton add_zero Set.image_congr Set.image_id' Finset.coe_singleton LinearIndepOn.zero_notMem_image Finset.dvd_lcm dvd_iff_exists_eq_mul_left Function.sometimes_spec Set.Finite.subset Set.finite_lt_nat Set.sep_subset_setOf Set.finite_Ico Set.ext Set.sep_and add_assoc add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instOrderedSub not_lt IsSemilinearSet.union IsSemilinearSet.of_finite IsSemilinearSet.add IsSemilinearSet.closure_finset

(root)

Definitions

Name	Category	Theorems
IsLinearSet 📖	MathDef	15 math math: Nat.isLinearSet_iff_exists_matrix, IsLinearSet.closure_finset, IsLinearSet.univ, IsLinearSet.exists_fg_eq_subtypeVal, isLinearSet_iff, IsProperLinearSet.isLinearSet, IsLinearSet.closure_of_finite, IsLinearSet.of_fg, IsLinearSet.vadd, isLinearSet_iff_exists_fg_eq_vadd, isSemilinearSet_iff, IsLinearSet.singleton, IsLinearSet.add, IsLinearSet.image, isLinearSet_iff_exists_fin_addMonoidHom
IsProperLinearSet 📖	MathDef	3 math math: isProperSemilinearSet_iff, IsProperLinearSet.singleton, isProperLinearSet_iff
IsProperSemilinearSet 📖	MathDef	9 math math: IsProperLinearSet.isProperSemilinearSet, IsProperSemilinearSet.empty, IsProperSemilinearSet.union, isProperSemilinearSet_iff, IsSemilinearSet.isProperSemilinearSet, IsProperSemilinearSet.sUnion, IsProperSemilinearSet.biUnion, IsProperSemilinearSet.biUnion_finset, IsLinearSet.isProperSemilinearSet
IsSemilinearSet 📖	MathDef	39 math math: IsSemilinearSet.biUnion_finset, FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize, IsSemilinearSet.closure_finset, IsSemilinearSet.compl, IsSemilinearSet.biInter_finset, IsSemilinearSet.biUnion, IsSemilinearSet.iUnion, IsSemilinearSet.exists_fg_eq_subtypeVal, IsSemilinearSet.biInter, Nat.isSemilinearSet_iff_ultimately_periodic, IsSemilinearSet.inter, IsSemilinearSet.image, IsProperSemilinearSet.isSemilinearSet, IsSemilinearSet.vadd, IsSemilinearSet.closure_of_finite, IsLinearSet.closure, IsSemilinearSet.exists_fg_eq_subtypeVal₂, IsSemilinearSet.of_finite, Nat.isSemilinearSet_setOf_mulVec_eq, IsSemilinearSet.diff, IsSemilinearSet.sUnion, IsSemilinearSet.iInter, isSemilinearSet_image_iff, IsSemilinearSet.singleton, isSemilinearSet_setOf_eq, IsSemilinearSet.add, isSemilinearSet_iff, IsSemilinearSet.sInter, IsSemilinearSet.preimage, IsSemilinearSet.univ, IsLinearSet.isSemilinearSet, IsSemilinearSet.closure, IsSemilinearSet.empty, IsSemilinearSet.of_fg, IsSemilinearSet.proj', IsSemilinearSet.union, FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear, IsSemilinearSet.proj, FirstOrder.Language.presburger.definable_iff_isSemilinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLinearSet_iff 📖	mathematical	—	IsLinearSet Finset HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instSetLike AddSubmonoid.closure Finset.instSetLike	—	Set.Finite.coe_toFinset
isLinearSet_iff_exists_fg_eq_vadd 📖	mathematical	—	IsLinearSet AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.FG HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction SetLike.coe AddSubmonoid.instSetLike	—	isLinearSet_iff
isProperLinearSet_iff 📖	mathematical	—	IsProperLinearSet Finset LinearIndepOn Nat.instSemiring AddCommMonoid.toNatModule SetLike.coe Finset.instSetLike HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction AddSubmonoid AddMonoid.toAddZeroClass AddSubmonoid.instSetLike AddSubmonoid.closure	—	Set.Finite.coe_toFinset Finset.finite_toSet
isProperSemilinearSet_iff 📖	mathematical	—	IsProperSemilinearSet Finset Set IsProperLinearSet Set.sUnion SetLike.coe Finset.instSetLike	—	Set.exists_finite_iff_finset
isSemilinearSet_iff 📖	mathematical	—	IsSemilinearSet Finset Set IsLinearSet Set.sUnion SetLike.coe Finset.instSetLike	—	Set.exists_finite_iff_finset
isSemilinearSet_image_iff 📖	mathematical	—	IsSemilinearSet Set.image DFunLike.coe EquivLike.toFunLike	—	Set.image_image Set.image_congr AddEquivClass.coe_symm_apply_apply Set.image_id' IsSemilinearSet.image AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass

---

← Back to Index