Theorems · Definition · logic and foundations
IsProperSemilinearSet
{M : Type u_1} → [AddCommMonoid M] → Set M → PropA semilinear set is proper if it is a finite union of proper linear sets.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommMonoidstatement and proof · cited by 12,281
- Set.Finiteproof · cited by 1,814
- Set.sUnionproof · cited by 392
- IsProperLinearSetproof · cited by 9
Cited by10
Results whose statement or proof uses this declaration.
- IsProperSemilinearSet.biUnionstatement and proof · cited by 2
- IsSemilinearSet.isProperSemilinearSetstatement and proof · cited by 1
- IsLinearSet.isProperSemilinearSetstatement and proof · cited by 1
- isProperSemilinearSet_iffstatement · cited by 1
- IsProperSemilinearSet.biUnion_finsetstatement and proof · cited by 1
- IsProperSemilinearSet.sUnionstatement and proof · cited by 1
- IsProperSemilinearSet.unionstatement and proof · cited by 1
- IsProperLinearSet.isProperSemilinearSetstatement · cited by 1
- IsProperSemilinearSet.emptystatement · cited by 0
- IsProperSemilinearSet.isSemilinearSetstatement and proof · cited by 0