Documentation Verification Report

HalesJewett

📁 Source: Mathlib/Combinatorics/HalesJewett.lean

Statistics

Metric	Count
Definitions `Line`, `AlmostMono`, `color`, `line`, `ColorFocused`, `focus`, `lines`, `IsMono`, `diagonal`, `horizontal`, `idxFun`, `instCoeFun`, `instInhabitedAlmostMonoDefaultOfNonempty`, `instInhabitedColorFocused`, `instInhabitedOfNonempty`, `map`, `prod`, `toFun`, `toSubspace`, `toSubspaceUnit`, `vertical`, `IsMono`, `idxFun`, `instCoeFun`, `instInhabited`, `reindex`, `toFun`	27
Theorems `has_color`, `distinct_colors`, `is_focused`, `toSubspace`, `toSubspaceUnit`, `apply_def`, `apply_none`, `apply_some`, `coe_apply`, `coe_injective`, `diagonal_apply`, `exists_mono_in_high_dimension`, `ext`, `ext_iff`, `horizontal_apply`, `map_apply`, `prod_apply`, `proper`, `toSubspaceUnit_apply`, `toSubspaceUnit_isMono`, `toSubspace_apply`, `toSubspace_isMono`, `vertical_apply`, `reindex`, `apply_def`, `apply_inl`, `apply_inr`, `coe_apply`, `coe_injective`, `exists_mono_in_high_dimension`, `exists_mono_in_high_dimension_fin`, `ext`, `ext_iff`, `proper`, `reindex_apply`, `reindex_isMono`, `exists_mono_homothetic_copy`	37
Total	64

Combinatorics

Definitions

Name	Category	Theorems
`Line` 📖	CompData	1 math math: `Line.coe_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mono_homothetic_copy` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`Line.exists_mono_in_high_dimension` `Finite.of_fintype` `Finset.card_pos` `Line.proper` `Finset.mem_filter` `Finset.mem_univ` `Finset.sum_add_sum_compl` `Finset.sum_const` `Finset.sum_congr` `Line.apply_none` `Finset.compl_filter`

Combinatorics.Line

Definitions

Name	Category	Theorems
`AlmostMono` 📖	CompData	1 math math: `ColorFocused.distinct_colors`
`ColorFocused` 📖	CompData	—
`IsMono` 📖	MathDef	3 math math: `toSubspaceUnit_isMono`, `exists_mono_in_high_dimension`, `toSubspace_isMono`
`diagonal` 📖	CompOp	1 math math: `diagonal_apply`
`horizontal` 📖	CompOp	1 math math: `horizontal_apply`
`idxFun` 📖	CompOp	4 math math: `coe_apply`, `proper`, `apply_def`, `ext_iff`
`instCoeFun` 📖	CompOp	—
`instInhabitedAlmostMonoDefaultOfNonempty` 📖	CompOp	—
`instInhabitedColorFocused` 📖	CompOp	—
`instInhabitedOfNonempty` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `map_apply`
`prod` 📖	CompOp	1 math math: `prod_apply`
`toFun` 📖	CompOp	14 math math: `diagonal_apply`, `vertical_apply`, `coe_injective`, `coe_apply`, `apply_none`, `ColorFocused.is_focused`, `prod_apply`, `toSubspaceUnit_apply`, `AlmostMono.has_color`, `apply_def`, `apply_some`, `map_apply`, `toSubspace_apply`, `horizontal_apply`
`toSubspace` 📖	CompOp	3 math math: `toSubspace_isMono`, `IsMono.toSubspace`, `toSubspace_apply`
`toSubspaceUnit` 📖	CompOp	3 math math: `toSubspaceUnit_isMono`, `IsMono.toSubspaceUnit`, `toSubspaceUnit_apply`
`vertical` 📖	CompOp	1 math math: `vertical_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_def` 📖	mathematical	—	`toFun` `idxFun`	—	—
`apply_none` 📖	mathematical	`idxFun`	`toFun`	—	—
`apply_some` 📖	mathematical	`idxFun`	`toFun`	—	—
`coe_apply` 📖	mathematical	—	`toFun` `idxFun`	—	—
`coe_injective` 📖	mathematical	—	`Combinatorics.Line` `toFun`	—	`ext` `exists_ne`
`diagonal_apply` 📖	mathematical	—	`toFun` `diagonal`	—	—
`exists_mono_in_high_dimension` 📖	mathematical	—	`IsMono`	—	`instFiniteULift`
`ext` 📖	—	`idxFun`	—	—	—
`ext_iff` 📖	mathematical	—	`idxFun`	—	`ext`
`horizontal_apply` 📖	mathematical	—	`toFun` `horizontal`	—	—
`map_apply` 📖	mathematical	—	`toFun` `map`	—	—
`prod_apply` 📖	mathematical	—	`toFun` `prod`	—	—
`proper` 📖	mathematical	—	`idxFun`	—	—
`toSubspaceUnit_apply` 📖	mathematical	—	`Combinatorics.Subspace.toFun` `toSubspaceUnit` `toFun`	—	—
`toSubspaceUnit_isMono` 📖	mathematical	—	`Combinatorics.Subspace.IsMono` `toSubspaceUnit` `IsMono`	—	`toSubspaceUnit_apply`
`toSubspace_apply` 📖	mathematical	—	`Combinatorics.Subspace.toFun` `toSubspace` `toFun`	—	—
`toSubspace_isMono` 📖	mathematical	—	`Combinatorics.Subspace.IsMono` `toSubspace` `IsMono`	—	`toSubspace_apply`
`vertical_apply` 📖	mathematical	—	`toFun` `vertical`	—	—

Combinatorics.Line.AlmostMono

Definitions

Name	Category	Theorems
`color` 📖	CompOp	2 math math: `has_color`, `Combinatorics.Line.ColorFocused.distinct_colors`
`line` 📖	CompOp	2 math math: `Combinatorics.Line.ColorFocused.is_focused`, `has_color`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`has_color` 📖	mathematical	—	`Combinatorics.Line.toFun` `line` `color`	—	—

Combinatorics.Line.ColorFocused

Definitions

Name	Category	Theorems
`focus` 📖	CompOp	1 math math: `is_focused`
`lines` 📖	CompOp	1 math math: `distinct_colors`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distinct_colors` 📖	mathematical	—	`Multiset.Nodup` `Multiset.map` `Combinatorics.Line.AlmostMono` `Combinatorics.Line.AlmostMono.color` `lines`	—	—
`is_focused` 📖	mathematical	`Combinatorics.Line.AlmostMono` `Multiset` `Multiset.instMembership` `lines`	`Combinatorics.Line.toFun` `Combinatorics.Line.AlmostMono.line` `focus`	—	—

Combinatorics.Line.IsMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSubspace` 📖	mathematical	`Combinatorics.Line.IsMono`	`Combinatorics.Subspace.IsMono` `Combinatorics.Line.toSubspace`	—	`Combinatorics.Line.toSubspace_isMono`
`toSubspaceUnit` 📖	mathematical	`Combinatorics.Line.IsMono`	`Combinatorics.Subspace.IsMono` `Combinatorics.Line.toSubspaceUnit`	—	`Combinatorics.Line.toSubspaceUnit_isMono`

Combinatorics.Subspace

Definitions

Name	Category	Theorems
`IsMono` 📖	MathDef	7 math math: `Combinatorics.Line.toSubspaceUnit_isMono`, `Combinatorics.Line.IsMono.toSubspaceUnit`, `exists_mono_in_high_dimension_fin`, `exists_mono_in_high_dimension`, `Combinatorics.Line.toSubspace_isMono`, `Combinatorics.Line.IsMono.toSubspace`, `reindex_isMono`
`idxFun` 📖	CompOp	4 math math: `coe_apply`, `proper`, `apply_def`, `ext_iff`
`instCoeFun` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`reindex` 📖	CompOp	3 math math: `IsMono.reindex`, `reindex_isMono`, `reindex_apply`
`toFun` 📖	CompOp	8 math math: `coe_injective`, `apply_inr`, `Combinatorics.Line.toSubspaceUnit_apply`, `coe_apply`, `Combinatorics.Line.toSubspace_apply`, `reindex_apply`, `apply_def`, `apply_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_def` 📖	mathematical	—	`toFun` `idxFun`	—	—
`apply_inl` 📖	mathematical	`idxFun`	`toFun`	—	—
`apply_inr` 📖	mathematical	`idxFun`	`toFun`	—	—
`coe_apply` 📖	mathematical	—	`toFun` `idxFun`	—	—
`coe_injective` 📖	mathematical	—	`Combinatorics.Subspace` `toFun`	—	`ext` `exists_ne` `exists_pair_ne` `Function.update_of_ne` `Function.update_self`
`exists_mono_in_high_dimension` 📖	mathematical	—	`IsMono`	—	`nonempty_fintype` `Countable.toSmall` `Finite.to_countable` `Combinatorics.Line.exists_mono_in_high_dimension` `Pi.finite` `Shrink.instFinite` `IsMono.reindex` `Combinatorics.Line.IsMono.toSubspace`
`exists_mono_in_high_dimension_fin` 📖	mathematical	—	`IsMono`	—	`exists_mono_in_high_dimension` `proper` `Equiv.symm_apply_apply`
`ext` 📖	—	`idxFun`	—	—	—
`ext_iff` 📖	mathematical	—	`idxFun`	—	`ext`
`proper` 📖	mathematical	—	`idxFun`	—	—
`reindex_apply` 📖	mathematical	—	`toFun` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Equiv.apply_symm_apply`
`reindex_isMono` 📖	mathematical	—	`IsMono` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`reindex_apply` `Equiv.forall_congr`

Combinatorics.Subspace.IsMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reindex` 📖	mathematical	`Combinatorics.Subspace.IsMono`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Combinatorics.Subspace.reindex`	—	`Equiv.symm_comp_self`

---

← Back to Index