Documentation Verification Report

Filter

📁 Source: Mathlib/Data/Analysis/Filter.lean

Statistics

Metric	Count
Definitions `CFilter`, `f`, `inf`, `instCoeFunForall`, `ofEquiv`, `pt`, `toFilter`, `toRealizer`, `Realizer`, `F`, `bind`, `bot`, `cofinite`, `comap`, `iSup`, `inf`, `instInhabitedPrincipal`, `map`, `ofEq`, `ofEquiv`, `ofFilter`, `principal`, `prod`, `sup`, `top`, `σ`, `instInhabitedCFilter`	27
Theorems `coe_mk`, `inf_le_left`, `inf_le_right`, `mem_toFilter_sets`, `ofEquiv_val`, `bot_F`, `bot_σ`, `eq`, `le_iff`, `map_F`, `map_σ`, `mem_sets`, `ne_bot_iff`, `ofEquiv_F`, `ofEquiv_σ`, `principal_F`, `principal_σ`, `tendsto_iff`, `top_F`, `top_σ`	20
Total	47

CFilter

Definitions

Name	Category	Theorems
`f` 📖	CompOp	15 math math: `Filter.Realizer.map_F`, `Filter.Realizer.ne_bot_iff`, `Ctop.Realizer.nhds_F`, `Filter.Realizer.mem_sets`, `Filter.Realizer.ofEquiv_F`, `mem_toFilter_sets`, `ofEquiv_val`, `Filter.Realizer.le_iff`, `Filter.Realizer.principal_F`, `inf_le_left`, `Filter.Realizer.bot_F`, `Filter.Realizer.top_F`, `inf_le_right`, `coe_mk`, `Filter.Realizer.tendsto_iff`
`inf` 📖	CompOp	2 math math: `inf_le_left`, `inf_le_right`
`instCoeFunForall` 📖	CompOp	—
`ofEquiv` 📖	CompOp	1 math math: `ofEquiv_val`
`pt` 📖	CompOp	—
`toFilter` 📖	CompOp	2 math math: `Filter.Realizer.eq`, `mem_toFilter_sets`
`toRealizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`f`	—	—
`inf_le_left` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `f` `inf`	—	—
`inf_le_right` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `f` `inf`	—	—
`mem_toFilter_sets` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `toFilter` `Set.instHasSubset` `f` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	—	—
`ofEquiv_val` 📖	mathematical	—	`f` `ofEquiv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—

Filter

Definitions

Name	Category	Theorems
`Realizer` 📖	CompData	—

Filter.Realizer

Definitions

Name	Category	Theorems
`F` 📖	CompOp	11 math math: `eq`, `map_F`, `ne_bot_iff`, `Ctop.Realizer.nhds_F`, `mem_sets`, `ofEquiv_F`, `le_iff`, `principal_F`, `bot_F`, `top_F`, `tendsto_iff`
`bind` 📖	CompOp	—
`bot` 📖	CompOp	2 math math: `bot_σ`, `bot_F`
`cofinite` 📖	CompOp	—
`comap` 📖	CompOp	—
`iSup` 📖	CompOp	—
`inf` 📖	CompOp	—
`instInhabitedPrincipal` 📖	CompOp	—
`map` 📖	CompOp	2 math math: `map_F`, `map_σ`
`ofEq` 📖	CompOp	—
`ofEquiv` 📖	CompOp	2 math math: `ofEquiv_F`, `ofEquiv_σ`
`ofFilter` 📖	CompOp	—
`principal` 📖	CompOp	2 math math: `principal_σ`, `principal_F`
`prod` 📖	CompOp	—
`sup` 📖	CompOp	—
`top` 📖	CompOp	2 math math: `top_F`, `top_σ`
`σ` 📖	CompOp	17 math math: `bot_σ`, `eq`, `map_F`, `ne_bot_iff`, `Ctop.Realizer.nhds_σ`, `Ctop.Realizer.nhds_F`, `principal_σ`, `mem_sets`, `ofEquiv_F`, `le_iff`, `principal_F`, `map_σ`, `bot_F`, `top_F`, `ofEquiv_σ`, `top_σ`, `tendsto_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_F` 📖	mathematical	—	`CFilter.f` `Set` `σ` `Bot.bot` `Filter` `Filter.instBot` `bot` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F` `Set.instEmptyCollection`	—	—
`bot_σ` 📖	mathematical	—	`σ` `Bot.bot` `Filter` `Filter.instBot` `bot`	—	—
`eq` 📖	mathematical	—	`CFilter.toFilter` `σ` `F`	—	—
`le_iff` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Set` `Set.instLE` `CFilter.f` `σ` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F`	—	`mem_sets` `Set.Subset.refl` `Set.Subset.trans`
`map_F` 📖	mathematical	—	`CFilter.f` `Set` `σ` `Filter.map` `map` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F` `Set.image`	—	—
`map_σ` 📖	mathematical	—	`σ` `Filter.map` `map`	—	—
`mem_sets` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `Set.instHasSubset` `CFilter.f` `σ` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F`	—	—
`ne_bot_iff` 📖	mathematical	—	`Set.Nonempty` `CFilter.f` `Set` `σ` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F`	—	`not_iff_comm` `le_bot_iff` `le_iff` `le_of_eq`
`ofEquiv_F` 📖	mathematical	—	`CFilter.f` `Set` `σ` `ofEquiv` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`ofEquiv_σ` 📖	mathematical	—	`σ` `ofEquiv`	—	—
`principal_F` 📖	mathematical	—	`CFilter.f` `Set` `σ` `Filter.principal` `principal` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F`	—	—
`principal_σ` 📖	mathematical	—	`σ` `Filter.principal` `principal`	—	—
`tendsto_iff` 📖	mathematical	—	`Filter.Tendsto` `Set` `Set.instMembership` `CFilter.f` `σ` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F`	—	`le_iff` `Set.image_subset_iff`
`top_F` 📖	mathematical	—	`CFilter.f` `Set` `σ` `Top.top` `Filter` `Filter.instTop` `top` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `F` `Set.univ`	—	—
`top_σ` 📖	mathematical	—	`σ` `Top.top` `Filter` `Filter.instTop` `top`	—	—

(root)

Definitions

Name	Category	Theorems
`CFilter` 📖	CompData	—
`instInhabitedCFilter` 📖	CompOp	—

---

← Back to Index