FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Clique.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 2 files
  1. lemma SimpleGraph.indepNum_of_isEmpty line 31 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, IsEmpty, Eq, Nat, SimpleGraph.indepNum, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, SupSet.sSup, Set.ofPred, Exists, Finset, SimpleGraph.IsNIndepSet, Singleton.singleton, Set, funext, And, SimpleGraph.IsIndepSet, EmptyCollection.emptyCollection, Finset.card, Subsingleton, EmptyCollection, Subsingleton.elim and 6 more

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  2. lemma SimpleGraph.indepNum_pos line 34 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, Finite, Nonempty, LT.lt, Nat, OfNat.ofNat, SimpleGraph.indepNum

    Proof uses: Fintype, Eq, nonempty_fintype, Nonempty.intro, Eq.mpr, LE.le, HAdd.hAdd, id, congrArg, Eq.symm, propext, Nat.add_one_le_iff, le_csSup, Set.ofPred, Exists, Finset, SimpleGraph.IsNIndepSet, Exists.intro, Membership.mem, Set and 25 more

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  3. def SimpleGraph.ecliqueNum line 45 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, ENat

    Proof uses: iSup, Finset, SimpleGraph.IsClique, Finset.card

    9 instances, coercions and auxiliary constants left out.

  4. def SimpleGraph.cliqueSizes The set of sizes of the cliques (maximal complete subgraphs) of G line 48 source

    Source documentation

    The set of sizes of the cliques (maximal complete subgraphs) of G.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: SimpleGraph, Set, Nat

    Proof uses: Set.ofPred, Exists, Finset, And, Maximal, SimpleGraph.IsClique, Eq, Finset.card

    5 instances, coercions and auxiliary constants left out.

    def cliqueSizes {V : Type} (G : SimpleGraph V) : Set ℕ :=
…
  5. def SimpleGraph.trianglesContaining The triangles of G containing the edge uv, that is, the 3-cliques of G whose vertex set contains both endpoints of uv line 54 source

    Source documentation

    The triangles of G containing the edge uv, that is, the 3-cliques of G whose vertex set contains both endpoints of uv.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, SimpleGraph, Sym2, Finset

    Proof uses: Finset.filter, LE.le, Sym2.toFinset, Classical.propDecidable, Eq, SimpleGraph.cliqueFinset, SimpleGraph.Adj, OfNat.ofNat, Nat

    5 instances, coercions and auxiliary constants left out.

    noncomputable def trianglesContaining {α : Type*} [Fintype α] (G : SimpleGraph α)
    (uv : Sym2 α) : Finset (Finset α) :=
…