Curry

📁 Source: Mathlib/Order/Filter/Curry.lean

Statistics

Metric	Count
Definitions Curry	1
Theorems curry, curry_le_prod, eventually_curry_iff, eventually_curry_prod_iff, frequently_curry_iff, frequently_curry_prod_iff, mem_curry_iff, prod_mem_curry	8
Total	9

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curry_le_prod 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder curry SProd.sprod instSProd	—	Eventually.curry
eventually_curry_iff 📖	mathematical	—	Eventually curry	—	—
eventually_curry_prod_iff 📖	mathematical	—	Eventually Set Set.instMembership SProd.sprod Set.instSProd curry Filter instMembership	—	—
frequently_curry_iff 📖	mathematical	—	Frequently curry	—	—
frequently_curry_prod_iff 📖	mathematical	—	Frequently Set Set.instMembership SProd.sprod Set.instSProd curry	—	—
mem_curry_iff 📖	mathematical	—	Set Filter instMembership curry Eventually Set.instMembership	—	—
prod_mem_curry 📖	mathematical	Set Filter instMembership	curry SProd.sprod Set.instSProd	—	curry_le_prod prod_mem_prod

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
curry 📖	mathematical	Filter.Eventually Filter.Tendsto	Function.HasUncurry.uncurry Function.hasUncurryInduction Function.hasUncurryBase Filter.curry	—	Filter.Eventually.mono

TypeVec

Definitions

Name	Category	Theorems
Curry 📖	CompOp	—

---

← Back to Index