Lax Lean Archive

Proof of `Contracting edges and right lexicographic products` (2nd statement)

groundedproofs/Lax871432Proofs/Results.lean · lax-871432

What this proof establishes

no assumptions

thm✓Lax871432.EdgeContractions (2nd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

prop:lexprod−contractprop:lexprod-contract, (1) ⇒ (2). In the formula for hom(F,G⋅H)hom(F, G ⋅ H) the factor depending on GG counts homomorphisms out of a quotient F/𝓡F / 𝓡, which is a contraction of FF and so lies in F\mathcal{F}.