Lax Lean Archive

Proof of `A Set of Jobs Is Feasible Exactly When It Satisfies Both Conditions` (1st statement)

groundedproofs/Lax496464Proofs/Section2.lean · lax-496464

What this proof establishes

no assumptions

thm✓Lax496464.Feasibility (1st 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

Transport FFJ.feasibleiffFFJ.feasible_iff along the bridge. Both conditions are definitionally the same on the two sides, so only the schedule structure has to be converted.