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	Set.image	—	Set.mem_image_of_mem IsAddFreimanHom.add_eq_add
mono 📖	—	Set Set.instHasSubset IsCorner	—	—	fst_fst_mem fst_snd_mem snd_fst_mem add_eq_add
of_image 📖	—	IsAddFreimanIso Set Set.instHasSubset SProd.sprod Set.instSProd Set.instMembership IsCorner Set.image	—	—	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	Set.image	—	isCornerFree_image
mono 📖	—	Set Set.instHasSubset IsCornerFree	—	—	IsCorner.mono
of_image 📖	—	IsAddFreimanHom Set.InjOn Set Set.instHasSubset SProd.sprod Set.instSProd IsCornerFree Set.image	—	—	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	3 math math: isCorner_iff, not_isCorner_empty, isCorner_image
IsCornerFree 📖	MathDef	7 math math: corners_theorem, corners_theorem_nat, isCornerFree_image, isCornerFree_empty, isCornerFree_iff, isCornerFree_singleton, Set.Subsingleton.isCornerFree

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