Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_fg_eq_subtypeVal`, `biInter`, `biInter_finset`, `compl`, `diff`, `exists_fg_eq_subtypeVal`, `exists_fg_eq_subtypeVal₂`, `iInter`, `inter`, `preimage`, `sInter`, `isLinearSet_iff_exists_matrix`, `isSemilinearSet_setOf_mulVec_eq`, `isLinearSet_iff_exists_fin_addMonoidHom`, `isSemilinearSet_setOf_eq`	15
Total	15

IsLinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_fg_eq_subtypeVal` 📖	mathematical	`IsLinearSet`	`AddSubmonoid.FG` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.toAddCommMonoid` `Set.image`	—	`AddSubmonoid.mem_closure_of_mem` `Set.mem_insert` `AddSubmonoid.fg_iff` `Set.Finite.insert` `Set.Finite.preimage` `Function.Injective.injOn` `Subtype.val_injective` `AddSubmonoid.coe_subtype` `Set.image_vadd_distrib` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.subtype_apply` `AddSubmonoid.coe_map` `AddMonoidHom.map_mclosure` `Set.ext` `Set.image_congr` `Set.mem_insert_of_mem`

IsSemilinearSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter` 📖	mathematical	`IsSemilinearSet`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.sInter_image` `sInter` `Set.Finite.image`
`biInter_finset` 📖	mathematical	`IsSemilinearSet`	`Set.iInter` `Finset` `Finset.instMembership`	—	`biInter` `Finset.finite_toSet`
`compl` 📖	mathematical	`IsSemilinearSet`	`Compl.compl` `Set` `Set.instCompl`	—	`Set.compl_eq_univ_diff` `diff` `univ`
`diff` 📖	mathematical	`IsSemilinearSet`	`Set` `Set.instSDiff`	—	`exists_fg_eq_subtypeVal₂` `Set.image_diff` `Subtype.val_injective` `image` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.fg_iff_exists_fin_addMonoidHom` `AddMonoid.fg_def` `AddMonoid.fg_iff_addSubmonoid_fg` `Set.image_preimage_eq` `AddMonoidHom.mrange_eq_top` `Set.preimage_diff` `Finite.of_fintype`
`exists_fg_eq_subtypeVal` 📖	mathematical	`IsSemilinearSet`	`AddSubmonoid.FG` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.toAddCommMonoid` `Set.image`	—	`le_iSup` `AddSubmonoid.FG.iSup` `iUnion` `image` `AddMonoidHom.instAddMonoidHomClass` `IsLinearSet.isSemilinearSet` `Set.sUnion_eq_iUnion` `Set.image_iUnion` `Set.image_image` `Set.image_congr` `AddSubmonoid.coe_inclusion` `Function.sometimes_spec` `IsLinearSet.exists_fg_eq_subtypeVal`
`exists_fg_eq_subtypeVal₂` 📖	mathematical	`IsSemilinearSet`	`AddSubmonoid.FG` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.toAddCommMonoid` `Set.image`	—	`exists_fg_eq_subtypeVal` `le_sup_left` `le_sup_right` `AddSubmonoid.FG.sup` `image` `AddMonoidHom.instAddMonoidHomClass` `Set.image_image` `Set.image_congr` `AddSubmonoid.coe_inclusion`
`iInter` 📖	mathematical	`IsSemilinearSet`	`Set.iInter`	—	`Set.sInter_range` `sInter` `Set.finite_range`
`inter` 📖	mathematical	`IsSemilinearSet`	`Set` `Set.instInter`	—	`exists_fg_eq_subtypeVal₂` `Set.image_inter` `Subtype.val_injective` `image` `AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.fg_iff_exists_fin_addMonoidHom` `AddMonoid.fg_def` `AddMonoid.fg_iff_addSubmonoid_fg` `Set.image_preimage_eq` `AddMonoidHom.mrange_eq_top` `Set.preimage_inter` `Finite.of_fintype`
`preimage` 📖	mathematical	`IsSemilinearSet`	`Set.preimage` `DFunLike.coe`	—	`AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.fg_iff_exists_fin_addMonoidHom` `AddMonoid.FG.fg_top` `Set.image_preimage_eq` `AddMonoidHom.mrange_eq_top` `image` `Set.preimage_comp` `AddMonoidHom.coe_coe` `AddMonoidHom.coe_comp` `Finite.of_fintype`
`sInter` 📖	mathematical	`IsSemilinearSet`	`Set.sInter`	—	`Set.Finite.induction_on` `Set.sInter_empty` `Set.sInter_insert` `inter`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearSet_iff_exists_matrix` 📖	mathematical	—	`IsLinearSet` `Pi.addCommMonoid` `instAddCommMonoid` `setOf` `Pi.instAdd` `Matrix.mulVec` `instNonUnitalNonAssocSemiring` `Fin.fintype`	—	`isLinearSet_iff_exists_fin_addMonoidHom` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `Set.ext` `LinearMap.toMatrix'_mulVec` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`isSemilinearSet_setOf_mulVec_eq` 📖	mathematical	—	`IsSemilinearSet` `Pi.addCommMonoid` `instAddCommMonoid` `setOf` `Pi.instAdd` `Matrix.mulVec` `instNonUnitalNonAssocSemiring`	—	`Finite.of_fintype` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLinearSet_iff_exists_fin_addMonoidHom` 📖	mathematical	—	`IsLinearSet` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `Set.range` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike`	—	`AddMonoidHom.instAddMonoidHomClass`
`isSemilinearSet_setOf_eq` 📖	mathematical	—	`IsSemilinearSet` `setOf` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe`	—	`AddMonoidHom.instAddMonoidHomClass` `AddSubmonoid.fg_iff_exists_fin_addMonoidHom` `AddMonoid.FG.fg_top` `Set.image_preimage_eq` `AddMonoidHom.mrange_eq_top` `Set.preimage_setOf_eq` `IsSemilinearSet.image` `Finite.of_fintype`

---

← Back to Index