Documentation Verification Report

VanishingFilter

📁 Source: FLT/Patching/VanishingFilter.lean

Statistics

Metric	Count
Definitions `vanishingFilter`, `vanishingFilterGI`, `vanishingUltrafilter`	3
Theorems `eventuallyProd_vanishingFilter_le`, `eventually_vanishingFilter_not_isUnit`, `mem_vanishingFilter`, `mem_vanishingUltrafilter`, `vanishingFilter_antimono`, `vanishingFilter_eventuallyProd`, `vanishingFilter_gc`, `vanishingFilter_le`	8
Total	11

(root)

Definitions

Name	Category	Theorems
`vanishingFilter` 📖	CompOp	7 math math: `eventuallyProd_vanishingFilter_le`, `vanishingFilter_antimono`, `vanishingFilter_gc`, `vanishingFilter_eventuallyProd`, `mem_vanishingFilter`, `eventually_vanishingFilter_not_isUnit`, `vanishingFilter_le`
`vanishingFilterGI` 📖	CompOp	—
`vanishingUltrafilter` 📖	CompOp	1 math math: `mem_vanishingUltrafilter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyProd_vanishingFilter_le` 📖	mathematical	—	`eventuallyProd` `vanishingFilter`	—	`vanishingFilter_gc`
`eventually_vanishingFilter_not_isUnit` 📖	mathematical	—	`vanishingFilter`	—	—
`mem_vanishingFilter` 📖	mathematical	—	`vanishingFilter`	—	—
`mem_vanishingUltrafilter` 📖	mathematical	—	`vanishingUltrafilter`	—	—
`vanishingFilter_antimono` 📖	mathematical	—	`vanishingFilter`	—	`vanishingFilter_gc`
`vanishingFilter_eventuallyProd` 📖	mathematical	—	`vanishingFilter` `eventuallyProd`	—	—
`vanishingFilter_gc` 📖	mathematical	—	`vanishingFilter` `eventuallyProd`	—	`vanishingFilter_le`
`vanishingFilter_le` 📖	mathematical	—	`vanishingFilter` `eventuallyProd`	—	—

---

← Back to Index