Fix

📁 Source: Mathlib/Control/Fix.lean

Statistics

Metric	Count
Definitions fix, approx, fix, fixAux, hasFix, hasFix	6
Theorems fix_def, fix_def'	2
Total	8

Fix

Definitions

Name	Category	Theorems
fix 📖	CompOp	1 math math: LawfulFix.fix_eq

Part

Definitions

Name	Category	Theorems
fix 📖	CompOp	9 math math: Fix.exists_fix_le_approx, Fix.approx_le_fix, fix_def, fix_def', fix_eq_ωSup, fix_eq_of_ωScottContinuous, Fix.mem_iff, fix_le, fix_eq_ωSup_of_ωScottContinuous
fixAux 📖	CompOp	—
hasFix 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fix_def 📖	mathematical	Dom Fix.approx	fix Nat.find	—	Nat.find_spec assert_pos Fix.approx.eq_2 fixAux.eq_1 assert_neg Nat.find_min
fix_def' 📖	mathematical	Dom Fix.approx	fix none	—	assert_neg

Part.Fix

Definitions

Name	Category	Theorems
approx 📖	CompOp	6 math math: exists_fix_le_approx, approx_mem_approxChain, approx_le_fix, approx_mono', mem_iff, approx_mono

Pi.Part

Definitions

Name	Category	Theorems
hasFix 📖	CompOp	—

---

← Back to Index