Commit 2026-02-03 17:15 e4be923d

View on Github →

feat(Order): teach fun_prop about ScottContinuous and friends (#33941) This PR adds the necessary lemmas and attributes for the fun_prop tactic to work with ωScottContinuous functions.

Estimated changes

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

deleted theorem CompleteLattice.ωScottContinuous.prodMk

modified def OmegaCompletePartialOrder.ContinuousHom.Prod.apply

modified def OmegaCompletePartialOrder.ContinuousHom.flip

added def OmegaCompletePartialOrder.ContinuousHom.ofFun

added theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous_apply

added theorem OmegaCompletePartialOrder.ωScottContinuous.apply

modified theorem OmegaCompletePartialOrder.ωScottContinuous.const

added theorem Prod.ωScottContinuous.prodMk

added theorem Prod.ωScottContinuous_fst

added theorem Prod.ωScottContinuous_snd

Modified Mathlib/Order/ScottContinuity.lean

added theorem ScottContinuous.comp

added theorem ScottContinuous.const

added theorem ScottContinuous.fst

modified theorem ScottContinuous.id

added theorem ScottContinuous.prodMk

added theorem ScottContinuous.snd

added theorem ScottContinuousOn.comp

added theorem ScottContinuousOn.const

added theorem ScottContinuousOn.fst

modified theorem ScottContinuousOn.id

added theorem ScottContinuousOn.image_comp

modified theorem ScottContinuousOn.prodMk

added theorem ScottContinuousOn.snd