OAI/Analysis/Pureness/Divisibility/
122 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- CommonMinorant.lean 3 declarations
- ContinuousCutTraceEnvelope.lean 5 declarations
- ContinuousSupportComparison.lean 2 declarations
- CornerComparison.lean 6 declarations
- CornerRanks.lean 4 declarations
- CutoffRank.lean 12 declarations
- ExtendedRankBudget.lean 5 declarations
- ExtendedSandwichRanks.lean 2 declarations
- FiniteContinuousDimension.lean 7 declarations
- FiniteCutComparison.lean 3 declarations
- FiniteLscComparison.lean 2 declarations
- Fullness.lean 2 declarations
- FullnessDensity.lean 1 declarations
- FullnessNormalization.lean 2 declarations
- FullnessPositiveSum.lean 1 declarations
- Hereditary.lean 10 declarations
- HereditaryApproximateUnit.lean 6 declarations
- HereditaryCuntz.lean 1 declarations
- HereditaryRank.lean 4 declarations
- HereditarySplitting.lean 6 declarations
- NonUnitalHereditaryBridge.lean 4 declarations
- NuclearAlmostDivisibility.lean 2 declarations
- NuclearCompletedFiniteComparison.lean 1 declarations
- NuclearFiniteComparison.lean 1 declarations
- NuclearFiniteFamilyAdditivity.lean 4 declarations
- NuclearStabilizedComparison.lean 2 declarations
- NuclearTracelessAlmostDivisibility.lean 2 declarations
- NuclearTracelessFiniteComparison.lean 3 declarations
- NuclearTracelessStabilizedComparison.lean 2 declarations
- RankBudget.lean 2 declarations
- SharedRankAddition.lean 5 declarations
- SharedSandwichGaps.lean 3 declarations
- SmallHereditaryRank.lean 2 declarations
- SmallTraceTransfer.lean 2 declarations
- SourceRankLimit.lean 3 declarations