Peel

📁 Source: Mathlib/Tactic/Peel.lean

Statistics

Metric	Count
Definitions applyPeelThm, mkFreshBinderName, peelArgs, peelArgsIff, peelCore, peelIffAux, peelUnbounded, quantifiers, throwPeelError, whnfQuantifier	10
Theorems and_imp_left_of_imp_imp, eventually_congr, eventually_imp, frequently_congr, frequently_imp	5
Total	15

Mathlib.Tactic.Peel

Definitions

Name	Category	Theorems
applyPeelThm 📖	CompOp	—
mkFreshBinderName 📖	CompOp	—
peelArgs 📖	CompOp	—
peelArgsIff 📖	CompOp	—
peelCore 📖	CompOp	—
peelIffAux 📖	CompOp	—
peelUnbounded 📖	CompOp	—
quantifiers 📖	CompOp	—
throwPeelError 📖	CompOp	—
whnfQuantifier 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
and_imp_left_of_imp_imp 📖	—	—	—	—	—
eventually_congr 📖	mathematical	—	Filter.Eventually	—	—
eventually_imp 📖	mathematical	Filter.Eventually	Filter.Eventually	—	Filter.Eventually.mp Filter.Eventually.of_forall
frequently_congr 📖	mathematical	—	Filter.Frequently	—	—
frequently_imp 📖	mathematical	Filter.Frequently	Filter.Frequently	—	Filter.Frequently.mp Filter.Eventually.of_forall

---

← Back to Index