CardinalInter

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

Statistics

Metric	Count
Definitions `CardinalInterFilter`, `CardinalGenerateSets`, `cardinalGenerate`, `ofCardinalInter`, `ofCardinalUnion`	5
Theorems `cardinal_sInter_mem`, `of_cardinalInterFilter_of_le`, `of_cardinalInterFilter_of_lt`, `toCountableInterFilter`, `toCardinalInterFilter`, `cardinal_bInter`, `cardinal_bUnion`, `cardinal_iInter`, `cardinal_iUnion`, `cardinal_bInter`, `cardinal_bUnion`, `cardinal_iInter`, `cardinal_iUnion`, `cardinalGenerate_isGreatest`, `cardinalInterFilter_aleph0`, `cardinalInterFilter_bot`, `cardinalInterFilter_inf`, `cardinalInterFilter_inf_eq`, `cardinalInterFilter_principal`, `cardinalInterFilter_sup`, `cardinalInterFilter_sup_eq`, `cardinalInterFilter_top`, `cardinalInter_ofCardinalGenerate`, `cardinalInter_ofCardinalInter`, `cardinalInter_ofCardinalUnion`, `cardinal_bInter_mem`, `cardinal_iInter_mem`, `eventually_cardinal_ball`, `eventually_cardinal_forall`, `instCardinalInterFilterComap`, `instCardinalInterFilterMap`, `le_cardinalGenerate_iff_of_cardinalInterFilter`, `mem_cardinalGenerate_iff`, `mem_cardinaleGenerate_iff`, `mem_ofCardinalInter`, `mem_ofCardinalUnion`, `cardinalInterFilter_aleph_one_iff`, `cardinal_sInter_mem`	38
Total	43

CardinalInterFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinal_sInter_mem` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Set` `Filter` `Filter.instMembership`	`Set.sInter`	—	—
`of_cardinalInterFilter_of_le` 📖	mathematical	`Cardinal` `Cardinal.instLE`	`CardinalInterFilter`	—	`cardinal_sInter_mem` `lt_of_lt_of_le`
`of_cardinalInterFilter_of_lt` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder`	`CardinalInterFilter`	—	`of_cardinalInterFilter_of_le` `LT.lt.le`
`toCountableInterFilter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Cardinal.aleph0`	`CountableInterFilter`	—	`cardinal_sInter_mem` `lt_of_le_of_lt` `Set.Countable.le_aleph0`

CountableInterFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCardinalInterFilter` 📖	mathematical	—	`CardinalInterFilter` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Cardinal.instLE` `instFunLikeOrderEmbedding` `Cardinal.aleph` `Ordinal.one`	—	`countable_sInter_mem` `Cardinal.countable_iff_lt_aleph_one`

Filter

Definitions

Name	Category	Theorems
`CardinalGenerateSets` 📖	CompData	—
`cardinalGenerate` 📖	CompOp	5 math math: `mem_cardinaleGenerate_iff`, `le_cardinalGenerate_iff_of_cardinalInterFilter`, `cardinalInter_ofCardinalGenerate`, `cardinalGenerate_isGreatest`, `mem_cardinalGenerate_iff`
`ofCardinalInter` 📖	CompOp	2 math math: `cardinalInter_ofCardinalInter`, `mem_ofCardinalInter`
`ofCardinalUnion` 📖	CompOp	2 math math: `cardinalInter_ofCardinalUnion`, `mem_ofCardinalUnion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalGenerate_isGreatest` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`IsGreatest` `Filter` `Preorder.toLE` `instPartialOrder` `setOf` `CardinalInterFilter` `Set` `Set.instHasSubset` `sets` `cardinalGenerate`	—	`Nat.instAtLeastTwoHAddOfNat` `cardinalInter_ofCardinalGenerate` `le_cardinalGenerate_iff_of_cardinalInterFilter`
`cardinalInterFilter_aleph0` 📖	mathematical	—	`CardinalInterFilter` `Cardinal.aleph0`	—	—
`cardinalInterFilter_bot` 📖	mathematical	—	`CardinalInterFilter` `Bot.bot` `Filter` `instBot`	—	`principal_empty` `cardinalInterFilter_principal`
`cardinalInterFilter_inf` 📖	mathematical	—	`CardinalInterFilter` `Filter` `instInf` `Cardinal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot`	—	`CardinalInterFilter.of_cardinalInterFilter_of_le` `inf_le_left` `inf_le_right` `cardinalInterFilter_inf_eq`
`cardinalInterFilter_inf_eq` 📖	mathematical	—	`CardinalInterFilter` `Filter` `instInf`	—	`cardinal_bInter_mem` `mem_of_superset` `inter_mem_inf` `Set.subset_sInter` `Set.inter_subset_inter` `Set.iInter_subset_of_subset` `Set.iInter_subset`
`cardinalInterFilter_principal` 📖	mathematical	—	`CardinalInterFilter` `principal`	—	`Set.subset_sInter`
`cardinalInterFilter_sup` 📖	mathematical	—	`CardinalInterFilter` `Filter` `instSup` `Cardinal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot`	—	`CardinalInterFilter.of_cardinalInterFilter_of_le` `inf_le_left` `inf_le_right` `cardinalInterFilter_sup_eq`
`cardinalInterFilter_sup_eq` 📖	mathematical	—	`CardinalInterFilter` `Filter` `instSup`	—	`cardinal_sInter_mem`
`cardinalInterFilter_top` 📖	mathematical	—	`CardinalInterFilter` `Top.top` `Filter` `instTop`	—	`principal_univ` `cardinalInterFilter_principal`
`cardinalInter_ofCardinalGenerate` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`CardinalInterFilter` `cardinalGenerate`	—	`Nat.instAtLeastTwoHAddOfNat` `cardinalInter_ofCardinalInter`
`cardinalInter_ofCardinalInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `Set.sInter`	`CardinalInterFilter` `ofCardinalInter`	—	`Nat.instAtLeastTwoHAddOfNat`
`cardinalInter_ofCardinalUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `Set.sUnion`	`CardinalInterFilter` `ofCardinalUnion`	—	`Nat.instAtLeastTwoHAddOfNat` `cardinalInter_ofCardinalInter`
`cardinal_bInter_mem` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem`	`Set` `Filter` `instMembership` `Set.iInter` `Set.instMembership`	—	`Set.biInter_eq_iInter` `cardinal_iInter_mem`
`cardinal_iInter_mem` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder`	`Set` `Filter` `instMembership` `Set.iInter`	—	`Set.sInter_range` `cardinal_sInter_mem` `lt_of_le_of_lt` `Cardinal.mk_range_le` `Set.forall_mem_range`
`eventually_cardinal_ball` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem`	`Eventually`	—	`Set.setOf_forall` `cardinal_bInter_mem`
`eventually_cardinal_forall` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder`	`Eventually`	—	`Set.setOf_forall` `cardinal_iInter_mem`
`instCardinalInterFilterComap` 📖	mathematical	—	`CardinalInterFilter` `comap`	—	`cardinal_bInter_mem` `Set.preimage_iInter` `Set.iInter₂_mono` `Function.sometimes_spec`
`instCardinalInterFilterMap` 📖	mathematical	—	`CardinalInterFilter` `map`	—	`Set.sInter_eq_biInter` `Set.preimage_iInter₂` `cardinal_bInter_mem`
`le_cardinalGenerate_iff_of_cardinalInterFilter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	`Filter` `Preorder.toLE` `instPartialOrder` `cardinalGenerate` `Set` `Set.instHasSubset` `sets`	—	`Nat.instAtLeastTwoHAddOfNat` `subset_trans` `Set.instIsTransSubset` `univ_mem` `mem_of_superset` `cardinal_sInter_mem`
`mem_cardinalGenerate_iff` 📖	mathematical	`Cardinal.IsRegular`	`Set` `Filter` `instMembership` `cardinalGenerate` `Cardinal.IsRegular.nat_lt` `Set.instHasSubset` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Set.sInter`	—	`Cardinal.IsRegular.nat_lt` `Set.singleton_subset_iff` `Cardinal.mk_fintype` `Fintype.card_unique` `Nat.cast_one` `Set.sInter_singleton` `Set.instReflSubset` `Set.empty_subset` `Cardinal.mk_eq_zero` `Set.instIsEmptyElemEmptyCollection` `Set.sInter_empty` `Cardinal.card_biUnion_lt_iff_forall_of_isRegular` `Set.subset_sInter` `subset_trans` `Set.instIsTransSubset` `Set.sInter_subset_sInter` `Set.subset_iUnion₂` `cardinalInter_ofCardinalGenerate` `mem_of_superset` `cardinal_sInter_mem`
`mem_cardinaleGenerate_iff` 📖	mathematical	`Cardinal.IsRegular`	`Set` `Filter` `instMembership` `cardinalGenerate` `Cardinal.IsRegular.nat_lt` `Set.instHasSubset` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Set.sInter`	—	`mem_cardinalGenerate_iff`
`mem_ofCardinalInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `Set.sInter`	`Filter` `instMembership` `ofCardinalInter`	—	`Nat.instAtLeastTwoHAddOfNat`
`mem_ofCardinalUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instOfNatAtLeastTwo` `Cardinal.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `Set.sUnion`	`Filter` `instMembership` `ofCardinalUnion` `Compl.compl` `Set.instCompl`	—	`Nat.instAtLeastTwoHAddOfNat`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinal_bInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Filter.EventuallyEq`	`Set.iInter` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.cardinal_bInter` `le` `symm`
`cardinal_bUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Filter.EventuallyEq`	`Set.iUnion` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.cardinal_bUnion` `le` `symm`
`cardinal_iInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Filter.EventuallyEq`	`Set.iInter`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.cardinal_iInter` `le` `symm`
`cardinal_iUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Filter.EventuallyEq`	`Set.iUnion`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.cardinal_iUnion` `le` `symm`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinal_bInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Filter.EventuallyLE` `Prop.le`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.biInter_eq_iInter` `cardinal_iInter`
`cardinal_bUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Filter.EventuallyLE` `Prop.le`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `cardinal_iUnion`
`cardinal_iInter` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Filter.EventuallyLE` `Prop.le`	`Set.iInter`	—	`Filter.Eventually.mono` `Filter.eventually_cardinal_forall` `Set.mem_iInter`
`cardinal_iUnion` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Filter.EventuallyLE` `Prop.le`	`Set.iUnion`	—	`Filter.Eventually.mono` `Filter.eventually_cardinal_forall` `Set.mem_iUnion`

(root)

Definitions

Name	Category	Theorems
`CardinalInterFilter` 📖	CompData	19 math math: `Filter.instCardinalInterFilter_cocardinal`, `Filter.cardinalInterFilter_inf_eq`, `Filter.cardinalInterFilter_bot`, `Filter.cardinalInterFilter_sup`, `Filter.cardinalInter_ofCardinalInter`, `CardinalInterFilter.of_cardinalInterFilter_of_le`, `Filter.instCardinalInterFilterMap`, `cardinalInterFilter_aleph_one_iff`, `Filter.cardinalInter_ofCardinalUnion`, `Filter.cardinalInterFilter_aleph0`, `Filter.cardinalInterFilter_principal`, `CardinalInterFilter.of_cardinalInterFilter_of_lt`, `Filter.cardinalInterFilter_top`, `Filter.cardinalInter_ofCardinalGenerate`, `CountableInterFilter.toCardinalInterFilter`, `Filter.cardinalInterFilter_inf`, `Filter.instCardinalInterFilterComap`, `Filter.cardinalInterFilter_sup_eq`, `Filter.cardinalGenerate_isGreatest`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalInterFilter_aleph_one_iff` 📖	mathematical	—	`CardinalInterFilter` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Cardinal.instLE` `instFunLikeOrderEmbedding` `Cardinal.aleph` `Ordinal.one` `CountableInterFilter`	—	`CardinalInterFilter.cardinal_sInter_mem` `Cardinal.countable_iff_lt_aleph_one` `CountableInterFilter.toCardinalInterFilter`
`cardinal_sInter_mem` 📖	mathematical	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Set.Elem` `Set`	`Filter` `Filter.instMembership` `Set.sInter`	—	`Filter.mem_of_superset` `Set.sInter_subset_of_mem` `CardinalInterFilter.cardinal_sInter_mem`

---

← Back to Index