Documentation Verification Report

LawfulFix

📁 Source: Mathlib/Control/LawfulFix.lean

Statistics

Metric	Count
Definitions `LawfulFix`, `toFix`, `approxChain`, `lawfulFix`, `toUnitMono`, `hasFix`, `lawfulFix`, `lawfulFix'`, `monotoneCurry`, `monotoneUncurry`	10
Theorems `fix_eq`, `approx_le_fix`, `approx_mem_approxChain`, `approx_mono`, `approx_mono'`, `exists_fix_le_approx`, `le_f_of_mem_approx`, `mem_iff`, `fix_eq_of_ωScottContinuous`, `fix_eq_ωSup`, `fix_eq_ωSup_of_ωScottContinuous`, `fix_le`, `toUnitMono_coe`, `ωScottContinuous_toUnitMono`, `monotoneCurry_coe`, `monotoneUncurry_coe`, `uncurry_curry_ωScottContinuous`, `ωScottContinuous_curry`, `ωScottContinuous_uncurry`	19
Total	29

LawfulFix

Definitions

Name	Category	Theorems
`toFix` 📖	CompOp	1 math math: `fix_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fix_eq` 📖	mathematical	`OmegaCompletePartialOrder.ωScottContinuous`	`Fix.fix` `toFix`	—	—

Part

Definitions

Name	Category	Theorems
`lawfulFix` 📖	CompOp	—
`toUnitMono` 📖	CompOp	2 math math: `toUnitMono_coe`, `ωScottContinuous_toUnitMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fix_eq_of_ωScottContinuous` 📖	mathematical	`OmegaCompletePartialOrder.ωScottContinuous` `instOmegaCompletePartialOrderForall` `Part` `omegaCompletePartialOrder`	`fix`	—	`OmegaCompletePartialOrder.ωScottContinuous.monotone` `fix_eq_ωSup_of_ωScottContinuous` `OmegaCompletePartialOrder.ωScottContinuous.map_ωSup` `le_antisymm` `OmegaCompletePartialOrder.ωSup_le_ωSup_of_le` `Fix.le_f_of_mem_approx` `le_refl`
`fix_eq_ωSup` 📖	mathematical	—	`fix` `DFunLike.coe` `OrderHom` `Pi.preorder` `Part` `PartialOrder.toPreorder` `instPartialOrder` `OrderHom.instFunLike` `OmegaCompletePartialOrder.ωSup` `instOmegaCompletePartialOrderForall` `omegaCompletePartialOrder` `Fix.approxChain`	—	`le_antisymm` `Fix.exists_fix_le_approx` `Fix.approx_mono'` `OmegaCompletePartialOrder.le_ωSup_of_le` `le_refl` `OmegaCompletePartialOrder.ωSup_le` `Fix.approx_le_fix`
`fix_eq_ωSup_of_ωScottContinuous` 📖	mathematical	`OmegaCompletePartialOrder.ωScottContinuous` `instOmegaCompletePartialOrderForall` `Part` `omegaCompletePartialOrder`	`fix` `OmegaCompletePartialOrder.ωSup` `Fix.approxChain` `Pi.preorder` `PartialOrder.toPreorder` `instPartialOrder` `OmegaCompletePartialOrder.ωScottContinuous.monotone`	—	`OmegaCompletePartialOrder.ωScottContinuous.monotone` `fix_eq_ωSup`
`fix_le` 📖	mathematical	`Pi.hasLe` `Part` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `DFunLike.coe` `OrderHom` `Pi.preorder` `OrderHom.instFunLike`	`fix`	—	`fix_eq_ωSup` `OmegaCompletePartialOrder.ωSup_le` `Fix.approx_mono` `bot_le` `OrderHom.monotone`
`toUnitMono_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Pi.preorder` `Part` `PartialOrder.toPreorder` `instPartialOrder` `OrderHom.instFunLike` `toUnitMono`	—	—
`ωScottContinuous_toUnitMono` 📖	mathematical	`OmegaCompletePartialOrder.ωScottContinuous` `Part` `omegaCompletePartialOrder`	`instOmegaCompletePartialOrderForall` `DFunLike.coe` `OrderHom` `Pi.preorder` `PartialOrder.toPreorder` `instPartialOrder` `OrderHom.instFunLike` `toUnitMono` `OmegaCompletePartialOrder.ωScottContinuous.monotone`	—	`OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom` `OmegaCompletePartialOrder.ωScottContinuous.monotone` `OmegaCompletePartialOrder.ωScottContinuous.map_ωSup` `OmegaCompletePartialOrder.Chain.map_comp`

Part.Fix

Definitions

Name	Category	Theorems
`approxChain` 📖	CompOp	3 math math: `approx_mem_approxChain`, `Part.fix_eq_ωSup`, `Part.fix_eq_ωSup_of_ωScottContinuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`approx_le_fix` 📖	mathematical	—	`Pi.hasLe` `Part` `Preorder.toLE` `PartialOrder.toPreorder` `Part.instPartialOrder` `approx` `DFunLike.coe` `OrderHom` `Pi.preorder` `OrderHom.instFunLike` `Part.fix`	—	`mem_iff`
`approx_mem_approxChain` 📖	mathematical	—	`OmegaCompletePartialOrder.Chain` `Pi.preorder` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder` `OmegaCompletePartialOrder.Chain.instMembership` `approxChain` `approx` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	`Stream'.mem_of_get_eq`
`approx_mono` 📖	mathematical	—	`Pi.hasLe` `Part` `Preorder.toLE` `PartialOrder.toPreorder` `Part.instPartialOrder` `approx` `DFunLike.coe` `OrderHom` `Pi.preorder` `OrderHom.instFunLike`	—	`le_rfl` `le_trans` `approx_mono'`
`approx_mono'` 📖	mathematical	—	`Pi.hasLe` `Part` `Preorder.toLE` `PartialOrder.toPreorder` `Part.instPartialOrder` `approx` `DFunLike.coe` `OrderHom` `Pi.preorder` `OrderHom.instFunLike`	—	`bot_le` `OrderHom.monotone`
`exists_fix_le_approx` 📖	mathematical	—	`Part` `Preorder.toLE` `PartialOrder.toPreorder` `Part.instPartialOrder` `Part.fix` `DFunLike.coe` `OrderHom` `Pi.preorder` `OrderHom.instFunLike` `approx`	—	`approx_le_fix` `Part.mem_unique` `mem_iff`
`le_f_of_mem_approx` 📖	mathematical	`OmegaCompletePartialOrder.Chain` `Pi.preorder` `Part` `PartialOrder.toPreorder` `Part.instPartialOrder` `OmegaCompletePartialOrder.Chain.instMembership` `approxChain`	`Pi.hasLe` `Preorder.toLE` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	`approx_mono'`
`mem_iff` 📖	mathematical	—	`Part` `Part.instMembership` `Part.fix` `DFunLike.coe` `OrderHom` `Pi.preorder` `PartialOrder.toPreorder` `Part.instPartialOrder` `OrderHom.instFunLike` `approx`	—	`Part.fix_def` `Nat.find_spec` `Part.dom_iff_mem` `approx_mono'` `approx_mono` `Part.mem_unique` `le_total` `Part.fix_def'`

Pi

Definitions

Name	Category	Theorems
`hasFix` 📖	CompOp	—
`lawfulFix` 📖	CompOp	—
`lawfulFix'` 📖	CompOp	—
`monotoneCurry` 📖	CompOp	3 math math: `monotoneCurry_coe`, `ωScottContinuous_curry`, `uncurry_curry_ωScottContinuous`
`monotoneUncurry` 📖	CompOp	3 math math: `ωScottContinuous_uncurry`, `monotoneUncurry_coe`, `uncurry_curry_ωScottContinuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monotoneCurry_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `preorder` `OrderHom.instFunLike` `monotoneCurry` `Sigma.curry`	—	—
`monotoneUncurry_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `preorder` `OrderHom.instFunLike` `monotoneUncurry` `Sigma.uncurry`	—	—
`uncurry_curry_ωScottContinuous` 📖	mathematical	`OmegaCompletePartialOrder.ωScottContinuous` `instOmegaCompletePartialOrderForall`	`DFunLike.coe` `OrderHom` `preorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `OrderHom.instFunLike` `OrderHom.comp` `monotoneUncurry` `OmegaCompletePartialOrder.ωScottContinuous.monotone` `monotoneCurry`	—	`OmegaCompletePartialOrder.ωScottContinuous.comp` `ωScottContinuous_uncurry` `ωScottContinuous_curry`
`ωScottContinuous_curry` 📖	mathematical	—	`OmegaCompletePartialOrder.ωScottContinuous` `instOmegaCompletePartialOrderForall` `DFunLike.coe` `OrderHom` `preorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `OrderHom.instFunLike` `monotoneCurry`	—	`OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom` `OmegaCompletePartialOrder.Chain.map_comp`
`ωScottContinuous_uncurry` 📖	mathematical	—	`OmegaCompletePartialOrder.ωScottContinuous` `instOmegaCompletePartialOrderForall` `DFunLike.coe` `OrderHom` `preorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `OrderHom.instFunLike` `monotoneUncurry`	—	`OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom` `OmegaCompletePartialOrder.Chain.map_comp`

(root)

Definitions

Name	Category	Theorems
`LawfulFix` 📖	CompData	—

---

← Back to Index