Finite

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

Statistics

Metric	Count
Definitions	0
Theorems `biInter`, `biUnion`, `iInter`, `iUnion`, `biInter`, `biUnion`, `iInter`, `iUnion`, `biInter_finset_mem`, `biInter_mem`, `eventually_all`, `eventually_all_finite`, `eventually_all_finset`, `eventually_subset_of_finite`, `exists_iInter_of_mem_iInf`, `frequently_exists`, `frequently_exists_finite`, `frequently_exists_finset`, `iInf_principal`, `iInf_principal'`, `iInf_principal_finite`, `iInf_principal_finset`, `iInf_sets_eq_finite`, `iInf_sets_eq_finite'`, `iInter_mem`, `mem_biInf_principal`, `mem_generate_iff`, `mem_iInf`, `mem_iInf'`, `mem_iInf_finite`, `mem_iInf_finite'`, `mem_iInf_finset`, `mem_iInf_of_finite`, `mem_iInf_of_iInter`, `sInter_mem`, `eventuallyEq_iInter`, `eventuallyEq_iUnion`, `eventuallyLE_iInter`, `eventuallyLE_iUnion`, `eventually_all`, `frequently_exists`, `iInter_mem_sets`, `exists_mem_filter_of_disjoint`, `eventuallyEq_iInter`, `eventuallyEq_iUnion`, `eventuallyLE_iInter`, `eventuallyLE_iUnion`, `eventually_all`, `frequently_exists`, `exists_mem_filter`	50
Total	50

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter_finset_mem` 📖	mathematical	—	`Set` `Filter` `instMembership` `Set.iInter` `Finset` `Finset.instMembership`	—	`biInter_mem` `Finset.finite_toSet`
`biInter_mem` 📖	mathematical	—	`Set` `Filter` `instMembership` `Set.iInter` `Set.instMembership`	—	`Set.Finite.induction_on` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `Set.iInter_iInter_eq_or_left`
`eventually_all` 📖	mathematical	—	`Eventually`	—	`Set.setOf_forall` `iInter_mem`
`eventually_all_finite` 📖	mathematical	—	`Eventually`	—	`Set.setOf_forall` `biInter_mem`
`eventually_all_finset` 📖	mathematical	—	`Eventually`	—	`Set.Finite.eventually_all` `Finset.finite_toSet`
`eventually_subset_of_finite` 📖	mathematical	`Eventually` `Set` `Set.instMembership`	`Set.instHasSubset`	—	`eventually_all_finite`
`exists_iInter_of_mem_iInf` 📖	mathematical	`Set` `Filter` `instMembership` `iInf` `instInfSet`	`Set.iInter`	—	`mem_iInf'` `iInf_range'` `Function.Surjective.iInter_comp` `Set.rangeFactorization_surjective`
`frequently_exists` 📖	mathematical	—	`Frequently`	—	`not_iff_not`
`frequently_exists_finite` 📖	mathematical	—	`Frequently` `Set` `Set.instMembership`	—	`not_iff_not`
`frequently_exists_finset` 📖	mathematical	—	`Frequently` `Finset` `Finset.instMembership`	—	`Set.Finite.frequently_exists` `Finset.finite_toSet`
`iInf_principal` 📖	mathematical	—	`iInf` `Filter` `instInfSet` `principal` `Set.iInter`	—	`nonempty_fintype` `instFinitePLift` `iInf_plift_down` `Set.iInter_plift_down` `iInf_congr_Prop` `iInf_pos` `Set.iInter_congr_Prop` `Set.iInter_true` `iInf_principal_finset`
`iInf_principal'` 📖	mathematical	—	`iInf` `Filter` `instInfSet` `principal` `Set.iInter`	—	`iInf_principal`
`iInf_principal_finite` 📖	mathematical	—	`iInf` `Filter` `instInfSet` `Set` `Set.instMembership` `principal` `Set.iInter`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `iInf_congr_Prop` `Set.iInter_congr_Prop` `iInf_principal_finset`
`iInf_principal_finset` 📖	mathematical	—	`iInf` `Filter` `instInfSet` `Finset` `Finset.instMembership` `principal` `Set.iInter`	—	`Finset.induction_on` `iInf_congr_Prop` `iInf_neg` `iInf_top` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `principal_univ` `Finset.iInf_insert` `Finset.set_biInter_insert` `inf_principal`
`iInf_sets_eq_finite` 📖	mathematical	—	`sets` `iInf` `Filter` `instInfSet` `Set.iUnion` `Set` `Finset` `Finset.instMembership`	—	`iInf_eq_iInf_finset` `iInf_sets_eq` `directed_of_isDirected_le` `Finset.isDirected_le` `biInf_mono`
`iInf_sets_eq_finite'` 📖	mathematical	—	`sets` `iInf` `Filter` `instInfSet` `Set.iUnion` `Set` `Finset` `Finset.instMembership`	—	`iInf_sets_eq_finite` `Function.Surjective.iInf_comp` `Equiv.surjective` `Equiv.plift_apply`
`iInter_mem` 📖	mathematical	—	`Set` `Filter` `instMembership` `Set.iInter`	—	`sInter_mem` `Set.finite_range` `Set.forall_mem_range`
`mem_biInf_principal` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `principal` `Set.Finite` `Set.instHasSubset` `Set.iInter` `Set.instMembership`	—	`mem_iInf` `instFiniteProp` `Set.Finite.inter_of_left` `Set.iInter_congr_Prop` `Set.iInter_and` `Set.biInter_eq_iInter` `Set.iInter_mono''` `mem_iInf_of_iInter` `iInf_congr_Prop` `iInf_pos` `Set.instReflSubset`
`mem_generate_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `generate` `Set.instHasSubset` `Set.Finite` `Set.sInter`	—	`Set.singleton_subset_iff` `Set.finite_singleton` `Eq.subset` `Set.instReflSubset` `Set.sInter_singleton` `Set.empty_subset` `Set.finite_empty` `Set.subset_univ` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.union_subset` `Set.Finite.union` `Set.sInter_union` `Set.inter_subset_inter` `mem_of_superset` `sInter_mem`
`mem_iInf` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Set.Finite` `Set.instMembership` `Set.iInter` `Set.Elem`	—	`iInf_eq_generate` `mem_generate_iff` `Set.eq_finite_iUnion_of_finite_subset_iUnion` `sInter_mem` `mem_of_superset` `Set.subset_union_right` `Set.union_iInter` `Set.union_eq_self_of_subset_right` `Set.sInter_iUnion` `mem_iInf_of_iInter` `Set.Subset.rfl`
`mem_iInf'` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Set.Finite` `Set.univ` `Set.iInter` `Set.instMembership`	—	`Set.biInter_eq_iInter` `univ_mem` `Subtype.coe_eta` `Subtype.coe_prop` `Set.iInter_dite` `Set.iInter_univ` `Set.inter_univ`
`mem_iInf_finite` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Finset` `Finset.instMembership`	—	`Set.ext_iff` `iInf_sets_eq_finite` `Set.mem_iUnion`
`mem_iInf_finite'` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Finset` `Finset.instMembership`	—	`Set.ext_iff` `iInf_sets_eq_finite'` `Set.mem_iUnion`
`mem_iInf_finset` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Finset` `Finset.instMembership` `Set.iInter`	—	`iInf_subtype'` `Set.biInter_eq_iInter` `mem_iInf_of_finite` `Finite.of_fintype` `Set.iInter_congr_of_surjective` `iInter_mem` `mem_iInf_of_mem`
`mem_iInf_of_finite` 📖	mathematical	—	`Set` `Filter` `instMembership` `iInf` `instInfSet` `Set.iInter`	—	`exists_iInter_of_mem_iInf` `iInter_mem` `mem_iInf_of_mem`
`mem_iInf_of_iInter` 📖	mathematical	`Set` `Filter` `instMembership` `Set.instMembership` `Set.instHasSubset` `Set.iInter` `Set.Elem`	`iInf` `instInfSet`	—	`mem_of_superset` `iInter_mem` `Finite.of_fintype` `mem_iInf_of_mem`
`sInter_mem` 📖	mathematical	—	`Set` `Filter` `instMembership` `Set.sInter`	—	`Set.sInter_eq_biInter` `biInter_mem`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.Finite.eventuallyEq_iInter`
`biUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.Finite.eventuallyEq_iUnion`
`iInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.iInter` `le` `symm`
`iUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.iUnion` `le` `symm`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter` `Set` `Set.instMembership`	—	`Set.Finite.eventuallyLE_iInter`
`biUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.Finite.eventuallyLE_iUnion`
`iInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter`	—	`Filter.Eventually.mono` `Filter.eventually_all` `Set.mem_iInter`
`iUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion`	—	`Filter.Eventually.mono` `Filter.eventually_all` `Set.mem_iUnion`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_iInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter` `Finset` `instMembership`	—	`Filter.EventuallyEq.biInter` `finite_toSet`
`eventuallyEq_iUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion` `Finset` `instMembership`	—	`Filter.EventuallyEq.biUnion` `finite_toSet`
`eventuallyLE_iInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter` `Finset` `instMembership`	—	`Filter.EventuallyLE.biInter` `finite_toSet`
`eventuallyLE_iUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion` `Finset` `instMembership`	—	`Filter.EventuallyLE.biUnion` `finite_toSet`
`eventually_all` 📖	mathematical	—	`Filter.Eventually`	—	`Filter.eventually_all_finset`
`frequently_exists` 📖	mathematical	—	`Filter.Frequently` `Finset` `instMembership`	—	`Filter.frequently_exists_finset`
`iInter_mem_sets` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `Set.iInter` `Finset` `instMembership`	—	`Filter.biInter_finset_mem`

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_filter_of_disjoint` 📖	mathematical	`Pairwise` `Function.onFun` `Filter` `Disjoint` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter`	`Set` `Filter.instMembership` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Filter.iInter_mem` `Filter.inter_mem` `Disjoint.mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.iInter_subset` `Set.inter_subset_left` `Set.inter_subset_right` `Function.sometimes_spec`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_iInter` 📖	mathematical	`Filter.EventuallyEq`	`Set.iInter` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.biInter` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`eventuallyEq_iUnion` 📖	mathematical	`Filter.EventuallyEq`	`Set.iUnion` `Set` `Set.instMembership`	—	`Filter.EventuallyLE.antisymm` `Filter.EventuallyLE.biUnion` `Filter.EventuallyEq.le` `Filter.EventuallyEq.symm`
`eventuallyLE_iInter` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iInter` `Set` `Set.instMembership`	—	`to_subtype` `Set.biInter_eq_iInter` `Filter.EventuallyLE.iInter`
`eventuallyLE_iUnion` 📖	mathematical	`Filter.EventuallyLE` `Prop.le`	`Set.iUnion` `Set` `Set.instMembership`	—	`to_subtype` `Set.biUnion_eq_iUnion` `Filter.EventuallyLE.iUnion`
`eventually_all` 📖	mathematical	—	`Filter.Eventually`	—	`Filter.eventually_all_finite`
`frequently_exists` 📖	mathematical	—	`Filter.Frequently` `Set` `Set.instMembership`	—	`Filter.frequently_exists_finite`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_filter` 📖	mathematical	`Set.PairwiseDisjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter`	`Set` `Filter.instMembership` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Pairwise.exists_mem_filter_of_disjoint` `Set.Finite.to_subtype` `Set.Pairwise.subtype` `CanLift.prf` `Pi.canLift` `Subtype.canLift` `Subtype.exists_pi_extension` `Pairwise.set_of_subtype`

---

← Back to Index