Documentation Verification Report

Defs

📁 Source: Mathlib/Combinatorics/Additive/Corner/Defs.lean

Statistics

Metric	Count
Definitions `IsCorner`, `IsCornerFree`	2
Theorems `add_eq_add`, `fst_fst_mem`, `fst_snd_mem`, `image`, `mono`, `of_image`, `snd_fst_mem`, `image`, `mono`, `of_image`, `isCornerFree`, `isCornerFree_empty`, `isCornerFree_iff`, `isCornerFree_image`, `isCornerFree_singleton`, `isCorner_iff`, `isCorner_image`, `not_isCorner_empty`	18
Total	20

IsCorner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_add` 📖	mathematical	`IsCorner`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`fst_fst_mem` 📖	mathematical	`IsCorner`	`Set` `Set.instMembership`	—	—
`fst_snd_mem` 📖	mathematical	`IsCorner`	`Set` `Set.instMembership`	—	—
`image` 📖	mathematical	`IsAddFreimanHom` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `IsCorner`	`IsCorner` `Set.image`	—	`Set.mem_image_of_mem` `IsAddFreimanHom.add_eq_add`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `IsCorner`	`IsCorner`	—	`fst_fst_mem` `fst_snd_mem` `snd_fst_mem` `add_eq_add`
`of_image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `Set.instMembership` `IsCorner` `Set.image`	`IsCorner`	—	`isCorner_image`
`snd_fst_mem` 📖	mathematical	`IsCorner`	`Set` `Set.instMembership`	—	—

IsCornerFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `IsCornerFree`	`IsCornerFree` `Set.image`	—	`isCornerFree_image`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `IsCornerFree`	`IsCornerFree`	—	`IsCorner.mono`
`of_image` 📖	mathematical	`IsAddFreimanHom` `Set.InjOn` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `IsCornerFree` `Set.image`	`IsCornerFree`	—	`IsCorner.fst_fst_mem` `IsCorner.snd_fst_mem` `IsCorner.image`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCornerFree` 📖	mathematical	`Set.Subsingleton`	`IsCornerFree`	—	`IsCorner.fst_fst_mem` `IsCorner.snd_fst_mem`

(root)

Definitions

Name	Category	Theorems
`IsCorner` 📖	CompData	6 math math: `isCorner_iff`, `IsCorner.image`, `IsCorner.mono`, `not_isCorner_empty`, `isCorner_image`, `IsCorner.of_image`
`IsCornerFree` 📖	MathDef	10 math math: `corners_theorem`, `IsCornerFree.image`, `corners_theorem_nat`, `isCornerFree_image`, `IsCornerFree.mono`, `isCornerFree_empty`, `isCornerFree_iff`, `isCornerFree_singleton`, `Set.Subsingleton.isCornerFree`, `IsCornerFree.of_image`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCornerFree_empty` 📖	mathematical	—	`IsCornerFree` `Set` `Set.instEmptyCollection`	—	`Set.Subsingleton.isCornerFree` `Set.subsingleton_empty`
`isCornerFree_iff` 📖	mathematical	`Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd`	`IsCornerFree`	—	`IsCorner.fst_fst_mem` `IsCorner.snd_fst_mem` `IsCorner.fst_snd_mem`
`isCornerFree_image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd`	`IsCornerFree` `Set.image`	—	`Set.MapsTo.image_subset` `Set.MapsTo.mono` `Set.MapsTo.prodMap` `Set.BijOn.mapsTo` `IsAddFreimanIso.bijOn` `Set.Subset.rfl` `isCornerFree_iff` `Set.BijOn.forall` `isCorner_image` `Set.InjOn.eq_iff` `Set.BijOn.injOn`
`isCornerFree_singleton` 📖	mathematical	—	`IsCornerFree` `Set` `Set.instSingletonSet`	—	`Set.Subsingleton.isCornerFree` `Set.subsingleton_singleton`
`isCorner_iff` 📖	mathematical	—	`IsCorner` `Set` `Set.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`isCorner_image` 📖	mathematical	`IsAddFreimanIso` `Set` `Set.instHasSubset` `SProd.sprod` `Set.instSProd` `Set.instMembership`	`IsCorner` `Set.image`	—	`Set.InjOn.prodMap` `Set.BijOn.injOn` `IsAddFreimanIso.bijOn` `isCorner_iff` `Set.InjOn.mem_image_iff` `Set.mk_mem_prod` `IsAddFreimanIso.add_eq_add`
`not_isCorner_empty` 📖	mathematical	—	`IsCorner` `Set` `Set.instEmptyCollection`	—	—

---

← Back to Index