Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GraphQuotient

Supporting results for pointwise provable equality.

Pointwise graph equality and quotient operations.

source
theorem PointwiseComposition.FailureOfComposition.ProofSearch.pointwise_equivalence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
Equivalence (Pointwise T)
source
theorem PointwiseComposition.FailureOfComposition.ProofSearch.comp_functional {F G : Graph} (hF : Functional F) (hG : Functional G) :
Functional (comp F G)
source
def PointwiseComposition.FailureOfComposition.ProofSearch.FunctionalGraph :
Type

The Functional Graph construction in FailureOfComposition.ProofSearch.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ProofSearch.functionalComp (F G : FunctionalGraph) :
    FunctionalGraph

    The functional Comp construction in FailureOfComposition.ProofSearch.

    Equations
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.ProofSearch.pointwiseSetoid (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
      Setoid FunctionalGraph

      The pointwise Setoid construction in FailureOfComposition.ProofSearch.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.ProofSearch.NoQuotientComposition (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        Prop

        The No Quotient Composition construction in FailureOfComposition.ProofSearch.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem PointwiseComposition.FailureOfComposition.ProofSearch.no_quotient_composition_of_graph_noncongruence (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : ∃ (F : Graph) (I : Graph) (G : Graph), Functional F ∧ Functional I ∧ Functional G ∧ Pointwise T F I ∧ ¬Pointwise T (comp F G) (comp I G)) :
          NoQuotientComposition T