Documentation Verification Report

Hindman

📁 Source: Mathlib/Combinatorics/Hindman.lean

Statistics

Metric	Count
Definitions `FP`, `cons`, `head`, `tail`, `FS`, `cons`, `head`, `tail`, `add`, `addSemigroup`, `mul`, `semigroup`	12
Theorems `finset_prod`, `mul`, `mul_two`, `singleton`, `FP_drop_subset_FP`, `FP_partition_regular`, `add`, `add_two`, `finset_sum`, `singleton`, `FS_iter_tail_sub_FS`, `FS_partition_regular`, `exists_FP_of_finite_cover`, `exists_FP_of_large`, `exists_FS_of_finite_cover`, `exists_FS_of_large`, `exists_idempotent_ultrafilter_le_FP`, `exists_idempotent_ultrafilter_le_FS`, `continuous_add_left`, `continuous_mul_left`, `eventually_add`, `eventually_mul`	22
Total	34

Hindman

Definitions

Name	Category	Theorems
`FP` 📖	CompData	7 math math: `exists_idempotent_ultrafilter_le_FP`, `exists_FP_of_finite_cover`, `FP.finset_prod`, `exists_FP_of_large`, `FP.singleton`, `FP.mul_two`, `FP_drop_subset_FP`
`FS` 📖	CompData	7 math math: `exists_idempotent_ultrafilter_le_FS`, `FS.finset_sum`, `exists_FS_of_finite_cover`, `FS.singleton`, `exists_FS_of_large`, `FS.add_two`, `FS_iter_tail_sub_FS`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FP_drop_subset_FP` 📖	mathematical	—	`Set` `Set.instHasSubset` `FP` `Stream'.drop`	—	`subset_refl` `Set.instReflSubset` `Stream'.drop_drop` `trans` `Set.instIsTransSubset`
`FP_partition_regular` 📖	mathematical	`Set` `Set.instHasSubset` `FP` `Set.sUnion`	`Set.instMembership`	—	`exists_idempotent_ultrafilter_le_FP` `Ultrafilter.finite_sUnion_mem_iff` `Filter.mem_of_superset` `exists_FP_of_large`
`FS_iter_tail_sub_FS` 📖	mathematical	—	`Set` `Set.instHasSubset` `FS` `Stream'.drop`	—	`subset_refl` `Set.instReflSubset` `Stream'.drop_drop` `trans` `Set.instIsTransSubset`
`FS_partition_regular` 📖	mathematical	`Set` `Set.instHasSubset` `FS` `Set.sUnion`	`Set.instMembership`	—	`exists_idempotent_ultrafilter_le_FS` `Ultrafilter.finite_sUnion_mem_iff` `Filter.mem_of_superset` `exists_FS_of_large`
`exists_FP_of_finite_cover` 📖	mathematical	`Set` `Set.instHasSubset` `Top.top` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra` `Set.sUnion`	`Set.instMembership` `FP`	—	`exists_idempotent_of_compact_t2_of_continuous_mul_left` `Ultrafilter.instNonempty` `ultrafilter_compact` `Ultrafilter.t2Space` `Ultrafilter.continuous_mul_left` `Ultrafilter.finite_sUnion_mem_iff` `Filter.mem_of_superset` `Filter.univ_mem` `exists_FP_of_large`
`exists_FP_of_large` 📖	mathematical	`Ultrafilter` `Ultrafilter.mul` `Semigroup.toMul` `Set` `Ultrafilter.instMembershipSet`	`Set.instHasSubset` `FP`	—	`Ultrafilter.nonempty_of_mem` `Filter.inter_mem` `Set.inter_subset_right` `Set.Nonempty.some_mem` `Stream'.corec_eq` `Stream'.head_cons` `Set.inter_subset_left` `Stream'.tail_cons`
`exists_FS_of_finite_cover` 📖	mathematical	`Set` `Set.instHasSubset` `Top.top` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra` `Set.sUnion`	`Set.instMembership` `FS`	—	`exists_idempotent_of_compact_t2_of_continuous_add_left` `Ultrafilter.instNonempty` `ultrafilter_compact` `Ultrafilter.t2Space` `Ultrafilter.continuous_add_left` `Ultrafilter.finite_sUnion_mem_iff` `Filter.mem_of_superset` `Filter.univ_mem` `exists_FS_of_large`
`exists_FS_of_large` 📖	mathematical	`Ultrafilter` `Ultrafilter.add` `AddSemigroup.toAdd` `Set` `Ultrafilter.instMembershipSet`	`Set.instHasSubset` `FS`	—	`Ultrafilter.nonempty_of_mem` `Filter.inter_mem` `Set.inter_subset_right` `Set.Nonempty.some_mem` `Stream'.corec_eq` `Stream'.head_cons` `Set.inter_subset_left` `Stream'.tail_cons`
`exists_idempotent_ultrafilter_le_FP` 📖	mathematical	—	`Ultrafilter` `Ultrafilter.mul` `Semigroup.toMul` `Filter.Eventually` `Set` `Set.instMembership` `FP` `Ultrafilter.toFilter`	—	`exists_idempotent_in_compact_subsemigroup` `Ultrafilter.t2Space` `Ultrafilter.continuous_mul_left` `IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed` `Filter.mp_mem` `Filter.univ_mem'` `Stream'.drop_drop` `Stream'.tail_eq_drop` `Filter.mem_pure` `IsClosed.isCompact` `ultrafilter_compact` `ultrafilter_isClosed_basic` `isClosed_iInter` `Set.mem_iInter` `Set.mem_setOf_eq` `Ultrafilter.eventually_mul` `FP.mul` `add_comm`
`exists_idempotent_ultrafilter_le_FS` 📖	mathematical	—	`Ultrafilter` `Ultrafilter.add` `AddSemigroup.toAdd` `Filter.Eventually` `Set` `Set.instMembership` `FS` `Ultrafilter.toFilter`	—	`exists_idempotent_in_compact_add_subsemigroup` `Ultrafilter.t2Space` `Ultrafilter.continuous_add_left` `IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed` `Filter.mp_mem` `Filter.univ_mem'` `Stream'.drop_drop` `Stream'.tail_eq_drop` `Filter.mem_pure` `IsClosed.isCompact` `ultrafilter_compact` `ultrafilter_isClosed_basic` `isClosed_iInter` `Set.mem_iInter` `Set.mem_setOf_eq` `Ultrafilter.eventually_add` `FS.add` `add_comm`

Hindman.FP

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	—
`head` 📖	CompOp	—
`tail` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finset_prod` 📖	mathematical	`Finset.Nonempty`	`Set` `Set.instMembership` `Hindman.FP` `Monoid.toSemigroup` `CommMonoid.toMonoid` `Finset.prod` `Stream'.get`	—	`Hindman.FP_drop_subset_FP` `Finset.eraseInduction` `Finset.mul_prod_erase` `Finset.min'_mem` `Stream'.head_drop` `Finset.eq_empty_or_nonempty` `Finset.prod_empty` `mul_one` `Stream'.tail_eq_drop` `Stream'.drop_drop` `add_comm` `Set.mem_of_subset_of_mem` `Finset.min'_lt_of_mem_erase_min'`
`mul` 📖	mathematical	`Set` `Set.instMembership` `Hindman.FP`	`Semigroup.toMul`	—	`mul_assoc`
`mul_two` 📖	mathematical	—	`Set` `Set.instMembership` `Hindman.FP` `Semigroup.toMul` `Stream'.get`	—	`Hindman.FP_drop_subset_FP` `Stream'.head_drop` `singleton` `Stream'.get_drop` `Stream'.tail_eq_drop`
`singleton` 📖	mathematical	—	`Set` `Set.instMembership` `Hindman.FP` `Stream'.get`	—	—

Hindman.FS

Definitions

Name	Category	Theorems
`cons` 📖	CompOp	—
`head` 📖	CompOp	—
`tail` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Set` `Set.instMembership` `Hindman.FS`	`AddSemigroup.toAdd`	—	`add_assoc`
`add_two` 📖	mathematical	—	`Set` `Set.instMembership` `Hindman.FS` `AddSemigroup.toAdd` `Stream'.get`	—	`Hindman.FS_iter_tail_sub_FS` `Stream'.head_drop` `singleton` `Stream'.get_drop` `Stream'.tail_eq_drop`
`finset_sum` 📖	mathematical	`Finset.Nonempty`	`Set` `Set.instMembership` `Hindman.FS` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `Finset.sum` `Stream'.get`	—	`Hindman.FS_iter_tail_sub_FS` `Finset.eraseInduction` `Finset.add_sum_erase` `Finset.min'_mem` `Stream'.head_drop` `Finset.eq_empty_or_nonempty` `Finset.sum_empty` `add_zero` `Stream'.tail_eq_drop` `Stream'.drop_drop` `add_comm` `Set.mem_of_subset_of_mem` `Finset.min'_lt_of_mem_erase_min'`
`singleton` 📖	mathematical	—	`Set` `Set.instMembership` `Hindman.FS` `Stream'.get`	—	—

Ultrafilter

Definitions

Name	Category	Theorems
`add` 📖	CompOp	3 math math: `Hindman.exists_idempotent_ultrafilter_le_FS`, `continuous_add_left`, `eventually_add`
`addSemigroup` 📖	CompOp	—
`mul` 📖	CompOp	3 math math: `Hindman.exists_idempotent_ultrafilter_le_FP`, `eventually_mul`, `continuous_mul_left`
`semigroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_add_left` 📖	mathematical	—	`Continuous` `Ultrafilter` `topologicalSpace` `add`	—	`TopologicalSpace.IsTopologicalBasis.continuous_iff` `ultrafilterBasis_is_basis` `Set.forall_mem_range` `ultrafilter_isOpen_basic`
`continuous_mul_left` 📖	mathematical	—	`Continuous` `Ultrafilter` `topologicalSpace` `mul`	—	`TopologicalSpace.IsTopologicalBasis.continuous_iff` `ultrafilterBasis_is_basis` `Set.forall_mem_range` `ultrafilter_isOpen_basic`
`eventually_add` 📖	mathematical	—	`Filter.Eventually` `toFilter` `Ultrafilter` `add`	—	—
`eventually_mul` 📖	mathematical	—	`Filter.Eventually` `toFilter` `Ultrafilter` `mul`	—	—

---

← Back to Index