OAI/Combinatorics/Sidorenko/Basic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SidorenkoCounterexample.faces line 7

   Also declared: ComparatorChallenges/SidorenkoCounterexample.lean:13 (same declaration text).

2. abbrev OAI.SidorenkoCounterexample.PatternVertex line 13

   Also declared: ComparatorChallenges/SidorenkoCounterexample.lean:19 (same declaration text).

3. def OAI.SidorenkoCounterexample.incidence line 15

   Distinct definitions of this name: ComparatorChallenges/SidorenkoCounterexample.lean:21 (different declaration text). Qualify references as OAI.SidorenkoCounterexample.incidence@path.

4. def OAI.SidorenkoCounterexample.H line 20

   Distinct definitions of this name: ComparatorChallenges/SidorenkoCounterexample.lean:26 (same statement text; different proof or body). Qualify references as OAI.SidorenkoCounterexample.H@path.

5. def OAI.SidorenkoCounterexample.homCount line 25

   Distinct definitions of this name: ComparatorChallenges/SidorenkoCounterexample.lean:31 (same statement text; different proof or body). Qualify references as OAI.SidorenkoCounterexample.homCount@path.

6. def OAI.SidorenkoCounterexample.homDensity line 28

   Also declared: ComparatorChallenges/SidorenkoCounterexample.lean:34 (same declaration text).

7. def OAI.SidorenkoCounterexample.edgeDensity line 31

   Also declared: ComparatorChallenges/SidorenkoCounterexample.lean:37 (same declaration text).