Documentation Verification Report

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`, `isLinearSet_iff`, `isLinearSet_iff_exists_fg_eq_vadd`, `isProperLinearSet_iff`, `isSemilinearSet_image_iff`	43
Total	47

IsLinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`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`	`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` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `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` `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`	`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`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_image` `sUnion` `Set.Finite.image`
`biUnion_finset` 📖	mathematical	`IsProperSemilinearSet`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`biUnion` `Finset.finite_toSet`
`empty` 📖	mathematical	—	`IsProperSemilinearSet` `Set` `Set.instEmptyCollection`	—	`instIsEmptyFalse` `Set.sUnion_empty`
`isSemilinearSet` 📖	mathematical	`IsProperSemilinearSet`	`IsSemilinearSet`	—	`IsProperLinearSet.isLinearSet`
`sUnion` 📖	mathematical	`IsProperSemilinearSet`	`Set.sUnion`	—	`Set.Finite.induction_on` `Set.sUnion_empty` `Set.sUnion_insert` `union`
`union` 📖	mathematical	`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`	`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`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_image` `sUnion` `Set.Finite.image`
`biUnion_finset` 📖	mathematical	`IsSemilinearSet`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`biUnion` `Finset.finite_toSet`
`closure` 📖	mathematical	`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`	`Set.iUnion`	—	`Set.sUnion_range` `sUnion` `Set.finite_range`
`image` 📖	mathematical	`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` `AddSubmonoid.instSetLike`	—	`IsLinearSet.isSemilinearSet` `IsLinearSet.of_fg`
`of_finite` 📖	mathematical	—	`IsSemilinearSet`	—	`Set.biUnion_of_singleton` `biUnion`
`proj` 📖	mathematical	`IsSemilinearSet` `Pi.addCommMonoid`	`setOf` `Set` `Set.instMembership`	—	`Set.ext` `image` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`proj'` 📖	—	`IsSemilinearSet` `Pi.addCommMonoid` `setOf`	—	—	`proj`
`sUnion` 📖	mathematical	`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`	`Set` `Set.instUnion`	—	`Set.sUnion_union` `Set.Finite.union` `Set.mem_union`
`univ` 📖	mathematical	—	`IsSemilinearSet` `Set.univ`	—	`IsLinearSet.isSemilinearSet` `IsLinearSet.univ`
`vadd` 📖	mathematical	`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`

(root)

Definitions

Name	Category	Theorems
`IsLinearSet` 📖	MathDef	10 math math: `Nat.isLinearSet_iff_exists_matrix`, `IsLinearSet.closure_finset`, `IsLinearSet.univ`, `isLinearSet_iff`, `IsProperLinearSet.isLinearSet`, `IsLinearSet.closure_of_finite`, `IsLinearSet.of_fg`, `isLinearSet_iff_exists_fg_eq_vadd`, `IsLinearSet.singleton`, `isLinearSet_iff_exists_fin_addMonoidHom`
`IsProperLinearSet` 📖	MathDef	2 math math: `IsProperLinearSet.singleton`, `isProperLinearSet_iff`
`IsProperSemilinearSet` 📖	MathDef	4 math math: `IsProperLinearSet.isProperSemilinearSet`, `IsProperSemilinearSet.empty`, `IsSemilinearSet.isProperSemilinearSet`, `IsLinearSet.isProperSemilinearSet`
`IsSemilinearSet` 📖	MathDef	13 math math: `IsSemilinearSet.closure_finset`, `IsProperSemilinearSet.isSemilinearSet`, `IsSemilinearSet.closure_of_finite`, `IsLinearSet.closure`, `IsSemilinearSet.of_finite`, `Nat.isSemilinearSet_setOf_mulVec_eq`, `isSemilinearSet_image_iff`, `IsSemilinearSet.singleton`, `isSemilinearSet_setOf_eq`, `IsSemilinearSet.univ`, `IsLinearSet.isSemilinearSet`, `IsSemilinearSet.empty`, `IsSemilinearSet.of_fg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearSet_iff` 📖	mathematical	—	`IsLinearSet` `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` `Finset.instSetLike`	—	`Set.Finite.coe_toFinset`
`isLinearSet_iff_exists_fg_eq_vadd` 📖	mathematical	—	`IsLinearSet` `AddSubmonoid.FG` `AddCommMonoid.toAddMonoid` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instSetLike`	—	`isLinearSet_iff`
`isProperLinearSet_iff` 📖	mathematical	—	`IsProperLinearSet` `LinearIndepOn` `Nat.instSemiring` `AddCommMonoid.toNatModule` `SetLike.coe` `Finset` `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`
`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