feat(Order/OmegaCompletePartialOrder): least fixed point and Scott induction#38316

tannerduve wants to merge 4 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

tannerduve:lfp-scott-inductiontannerduve/mathlib4:lfp-scott-inductionCopy head branch name to clipboard