FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.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

6 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. def SimpleGraph.largestInducedForestSize largestInducedForestSize G is the size of a largest induced forest of G line 28 source

    Source documentation

    largestInducedForestSize G is the size of a largest induced forest of G.

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

    Statement uses: SimpleGraph, Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, And, SimpleGraph.IsAcyclic, SimpleGraph.induce, Eq, Finset.card

    4 instances, coercions and auxiliary constants left out.

    noncomputable def largestInducedForestSize (G : SimpleGraph α) : ℕ :=
…
  2. def SimpleGraph.largestInducedBipartiteSubgraphSize largestInducedBipartiteSubgraphSize G is the size of a largest induced bipartite subgraph of G line 33 source

    Source documentation

    largestInducedBipartiteSubgraphSize G is the size of a largest induced bipartite subgraph of G.

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

    Statement uses: SimpleGraph, Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, And, SimpleGraph.IsBipartite, SimpleGraph.induce, Eq, Finset.card

    4 instances, coercions and auxiliary constants left out.

    noncomputable def largestInducedBipartiteSubgraphSize (G : SimpleGraph α) : ℕ :=
…
  3. theorem SimpleGraph.induce_isBipartite_iff_exists_coloring An induced subgraph is bipartite exactly when its vertices admit a two-coloring line 38 source

    Source documentation

    An induced subgraph is bipartite exactly when its vertices admit a two-coloring.

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

    Statement uses: DecidableEq, SimpleGraph, Finset, Iff, SimpleGraph.IsBipartite, SimpleGraph.induce, Exists, Fin, OfNat.ofNat, Nat, Membership.mem, SimpleGraph.Adj, Ne

    Proof uses: Iff.intro, SimpleGraph.Coloring, Exists.intro, dite, SimpleGraph.completeGraph, Subtype.mk, Set, Not, Eq.mpr, id, Eq, congr, congrArg, Decidable, dif_pos, SimpleGraph.Coloring.valid, Nonempty.intro, SimpleGraph.Coloring.mk, Subtype.prop

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

    theorem induce_isBipartite_iff_exists_coloring (G : SimpleGraph α) (s : Finset α) :
    (G.induce s).IsBipartite ↔
      ∃ c : α → Fin 2, ∀ u ∈ s, ∀ v ∈ s, G.Adj u v → c u ≠ c v := by
…

    Mentions: c

  4. def SimpleGraph.computableLargestInducedBipartiteSubgraphSize Computable largest induced bipartite subgraph size via powerset enumeration line 51 source

    Source documentation

    Computable largest induced bipartite subgraph size via powerset enumeration.

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat

    Proof uses: Finset.sup, Finset, Finset.filter, Exists, Fin, OfNat.ofNat, Membership.mem, Ne, Eq, Finset.powerset, Finset.univ, Finset.card

    14 instances, coercions and auxiliary constants left out.

    def computableLargestInducedBipartiteSubgraphSize (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
  5. theorem SimpleGraph.largestInducedBipartiteSubgraphSize_eq_computable The computable largest induced bipartite subgraph size agrees with the sSup definition line 56 source

    Source documentation

    The computable largest induced bipartite subgraph size agrees with the sSup definition.

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

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.largestInducedBipartiteSubgraphSize, SimpleGraph.computableLargestInducedBipartiteSubgraphSize

    Proof uses: id, SupSet.sSup, Set.ofPred, Exists, Finset, And, SimpleGraph.IsBipartite, SimpleGraph.induce, Finset.card, le_antisymm, Finset.sup, Finset.filter, Fin, OfNat.ofNat, Membership.mem, Ne, Finset.powerset, Finset.univ, csSup_le, Exists.intro and 33 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

    theorem largestInducedBipartiteSubgraphSize_eq_computable
    (G : SimpleGraph α) [DecidableRel G.Adj] :
    G.largestInducedBipartiteSubgraphSize = G.computableLargestInducedBipartiteSubgraphSize := by
…
  6. def SimpleGraph.b b G is the number of vertices of a largest induced bipartite subgraph of G line 78 source

    Source documentation

    b G is the number of vertices of a largest induced bipartite subgraph of G. Returned as a real number.

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

    Statement uses: SimpleGraph, Real

    Proof uses: SimpleGraph.largestInducedBipartiteSubgraphSize

    2 instances, coercions and auxiliary constants left out.

    noncomputable def b (G : SimpleGraph α) : ℝ :=
…