ValuedCSP

📁 Source: Mathlib/Combinatorics/Optimization/ValuedCSP.lean

Statistics

Metric	Count
Definitions FractionalOperation, IsFractionalPolymorphismFor, IsSymmetric, IsSymmetricFractionalPolymorphismFor, IsValid, size, tt, AdmitsFractional, HasMaxCutProperty, HasMaxCutPropertyAt, Instance, IsOptimumSolution, evalSolution, app, evalSolution, f, n	17
Theorems contains, forbids_commutativeFractionalPolymorphism, rows_lt_aux, inΓ	4
Total	21

FractionalOperation

Definitions

Name	Category	Theorems
IsFractionalPolymorphismFor 📖	MathDef	—
IsSymmetric 📖	MathDef	—
IsSymmetricFractionalPolymorphismFor 📖	MathDef	—
IsValid 📖	MathDef	—
size 📖	CompOp	—
tt 📖	CompOp	—

FractionalOperation.IsValid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contains 📖	mathematical	FractionalOperation.IsValid	FractionalOperation Multiset.instMembership	—	Multiset.exists_mem_of_ne_zero

Function

Definitions

Name	Category	Theorems
AdmitsFractional 📖	MathDef	1 math math: HasMaxCutProperty.forbids_commutativeFractionalPolymorphism
HasMaxCutProperty 📖	MathDef	—
HasMaxCutPropertyAt 📖	MathDef	—

Function.HasMaxCutProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forbids_commutativeFractionalPolymorphism 📖	mathematical	Function.HasMaxCutProperty FractionalOperation.IsValid FractionalOperation.IsSymmetric	Function.AdmitsFractional	—	Multiset.sum_lt_sum le_of_lt Function.HasMaxCutPropertyAt.rows_lt_aux FractionalOperation.IsValid.contains two_nsmul add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add Multiset.map_const' Multiset.map_congr Multiset.map_map lt_of_lt_of_le Fin.sum_univ_two' nsmul_left_comm Multiset.sum_replicate ne_of_lt

Function.HasMaxCutPropertyAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rows_lt_aux 📖	mathematical	Function.HasMaxCutPropertyAt FractionalOperation.IsSymmetric Multiset Multiset.instMembership FractionalOperation.tt Matrix.vecCons Matrix.vecEmpty	Preorder.toLT PartialOrder.toPreorder	—	Matrix.cons_val_succ Matrix.cons_val_fin_one lt_of_le_of_ne Multiset.mem_map FractionalOperation.tt.eq_1 Matrix.cons_val' Matrix.const_fin1_eq

ValuedCSP

Definitions

Name	Category	Theorems
Instance 📖	CompOp	—

ValuedCSP.Instance

Definitions

Name	Category	Theorems
IsOptimumSolution 📖	MathDef	—
evalSolution 📖	CompOp	—

ValuedCSP.Term

Definitions

Name	Category	Theorems
app 📖	CompOp	—
evalSolution 📖	CompOp	—
f 📖	CompOp	1 math math: inΓ
n 📖	CompOp	1 math math: inΓ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inΓ 📖	mathematical	—	ValuedCSP Set.instMembership n f	—	—

(root)

Definitions

Name	Category	Theorems
FractionalOperation 📖	CompOp	1 math math: FractionalOperation.IsValid.contains

---

← Back to Index