Documentation Verification Report

CountableInter

📁 Source: Mathlib/Order/Filter/CountableInter.lean

Statistics

Metric	Count
Definitions `CountableInterFilter`, `CountableGenerateSets`, `countableGenerate`, `instCountableInterFilterCountableGenerate`, `ofCountableInter`, `ofCountableUnion`	6
Theorems `countable_sInter_mem`, `curry`, `countable_bInter`, `countable_bUnion`, `countable_iInter`, `countable_iUnion`, `countable_bInter`, `countable_bUnion`, `countable_iInter`, `countable_iUnion`, `countableGenerate_isGreatest`, `countableInter_ofCountableInter`, `countableInter_ofCountableUnion`, `le_countableGenerate_iff_of_countableInterFilter`, `mem_countableGenerate_iff`, `mem_ofCountableInter`, `mem_ofCountableUnion`, `countableInterFilter_bot`, `countableInterFilter_inf`, `countableInterFilter_principal`, `countableInterFilter_sup`, `countableInterFilter_top`, `countable_bInter_mem`, `countable_iInter_mem`, `countable_sInter_mem`, `eventually_countable_ball`, `eventually_countable_forall`, `instCountableInterFilterComap`, `instCountableInterFilterMap`	29
Total	35

CountableInterFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_sInter_mem` 📖	mathematical	`Set` `Filter` `Filter.instMembership`	`Set.sInter`	—	—
`curry` 📖	mathematical	—	`CountableInterFilter` `Filter.curry`	—	`eventually_countable_ball`

EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_bInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `EventuallyLE.countable_bInter` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`countable_bUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `EventuallyLE.countable_bUnion` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`countable_iInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter`	—	`Filter.EventuallyLE.antisymm` `EventuallyLE.countable_iInter` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`countable_iUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion`	—	`Filter.EventuallyLE.antisymm` `EventuallyLE.countable_iUnion` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`

EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable_bInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.biInter_eq_iInter` `countable_iInter` `Encodable.countable`
`countable_bUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `countable_iUnion` `Encodable.countable`
`countable_iInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter`	—	`Filter.Eventually.mono` `eventually_countable_forall` `Set.mem_iInter`
`countable_iUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion`	—	`Filter.Eventually.mono` `eventually_countable_forall` `Set.mem_iUnion`

Filter

Definitions

Name	Category	Theorems
`CountableGenerateSets` 📖	CompData	—
`countableGenerate` 📖	CompOp	3 math math: `mem_countableGenerate_iff`, `countableGenerate_isGreatest`, `le_countableGenerate_iff_of_countableInterFilter`
`instCountableInterFilterCountableGenerate` 📖	CompOp	—
`ofCountableInter` 📖	CompOp	2 math math: `countableInter_ofCountableInter`, `mem_ofCountableInter`
`ofCountableUnion` 📖	CompOp	2 math math: `countableInter_ofCountableUnion`, `mem_ofCountableUnion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableGenerate_isGreatest` 📖	mathematical	—	`IsGreatest` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `setOf` `CountableInterFilter` `Set` `Set.instHasSubset` `sets` `countableGenerate`	—	`le_countableGenerate_iff_of_countableInterFilter`
`countableInter_ofCountableInter` 📖	mathematical	`Set` `Set.instMembership` `Set.sInter`	`CountableInterFilter` `ofCountableInter`	—	—
`countableInter_ofCountableUnion` 📖	mathematical	`Set` `Set.instMembership` `Set.sUnion`	`CountableInterFilter` `ofCountableUnion`	—	`countableInter_ofCountableInter`
`le_countableGenerate_iff_of_countableInterFilter` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `countableGenerate` `Set` `Set.instHasSubset` `sets`	—	`subset_trans` `Set.instIsTransSubset` `univ_mem` `mem_of_superset` `countable_sInter_mem`
`mem_countableGenerate_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `countableGenerate` `Set.instHasSubset` `Set.Countable` `Set.sInter`	—	`Set.sInter_singleton` `Set.instReflSubset` `Set.sInter_empty` `Set.Countable.biUnion` `Set.subset_sInter` `subset_trans` `Set.instIsTransSubset` `Set.sInter_subset_sInter` `Set.subset_iUnion₂` `mem_of_superset` `countable_sInter_mem`
`mem_ofCountableInter` 📖	mathematical	`Set` `Set.instMembership` `Set.sInter`	`Filter` `instMembership` `ofCountableInter`	—	—
`mem_ofCountableUnion` 📖	mathematical	`Set` `Set.instMembership` `Set.sUnion`	`Filter` `instMembership` `ofCountableUnion` `Compl.compl` `Set.instCompl`	—	—

(root)

Definitions

Name	Category	Theorems
`CountableInterFilter` 📖	CompData	15 math math: `CardinalInterFilter.toCountableInterFilter`, `instCountableInterFilterMap`, `countableInterFilter_residual`, `Filter.countableInter_ofCountableUnion`, `countableInterFilter_sup`, `MeasureTheory.instCountableInterFilter`, `Filter.countableGenerate_isGreatest`, `cardinalInterFilter_aleph_one_iff`, `countableInterFilter_inf`, `Filter.countableInter_ofCountableInter`, `countableInterFilter_top`, `CountableInterFilter.curry`, `countableInterFilter_principal`, `instCountableInterFilterComap`, `countableInterFilter_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableInterFilter_bot` 📖	mathematical	—	`CountableInterFilter` `Bot.bot` `Filter` `Filter.instBot`	—	`Filter.principal_empty` `countableInterFilter_principal`
`countableInterFilter_inf` 📖	mathematical	—	`CountableInterFilter` `Filter` `Filter.instInf`	—	`countable_bInter_mem` `Filter.mem_of_superset` `Filter.inter_mem_inf` `Set.subset_sInter` `Set.inter_subset_inter` `Set.iInter_subset_of_subset` `Set.iInter_subset`
`countableInterFilter_principal` 📖	mathematical	—	`CountableInterFilter` `Filter.principal`	—	`Set.subset_sInter`
`countableInterFilter_sup` 📖	mathematical	—	`CountableInterFilter` `Filter` `Filter.instSup`	—	`countable_sInter_mem`
`countableInterFilter_top` 📖	mathematical	—	`CountableInterFilter` `Top.top` `Filter` `Filter.instTop`	—	`Filter.principal_univ` `countableInterFilter_principal`
`countable_bInter_mem` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `Set.iInter` `Set.instMembership`	—	`Set.biInter_eq_iInter` `countable_iInter_mem` `Encodable.countable`
`countable_iInter_mem` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `Set.iInter`	—	`countable_sInter_mem` `Set.countable_range` `Set.forall_mem_range` `Set.sInter_range`
`countable_sInter_mem` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `Set.sInter`	—	`Filter.mem_of_superset` `Set.sInter_subset_of_mem` `CountableInterFilter.countable_sInter_mem`
`eventually_countable_ball` 📖	mathematical	—	`Filter.Eventually`	—	`Set.setOf_forall` `countable_bInter_mem`
`eventually_countable_forall` 📖	mathematical	—	`Filter.Eventually`	—	`Set.setOf_forall` `countable_iInter_mem`
`instCountableInterFilterComap` 📖	mathematical	—	`CountableInterFilter` `Filter.comap`	—	`countable_bInter_mem` `Set.preimage_iInter` `Set.iInter₂_mono` `Function.sometimes_spec`
`instCountableInterFilterMap` 📖	mathematical	—	`CountableInterFilter` `Filter.map`	—	`Set.sInter_eq_biInter` `Set.preimage_iInter₂` `countable_bInter_mem`

---

← Back to Index