ApplyFun

📁 Source: Mathlib/Tactic/ApplyFun.lean

Statistics

Metric	Count
Definitions applyFun, applyFunHyp, applyFunTarget, applyFunTargetFailure, maybeProveInjective	5
Theorems le_of_le, lt_of_lt	2
Total	7

Mathlib.Tactic

Definitions

Name	Category	Theorems
applyFun 📖	CompOp	—
applyFunHyp 📖	CompOp	—
applyFunTarget 📖	CompOp	—
applyFunTargetFailure 📖	CompOp	—
maybeProveInjective 📖	CompOp	—

Mathlib.Tactic.ApplyFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_le 📖	—	DFunLike.coe OrderIso instFunLikeOrderIso	—	—	OrderIso.le_iff_le
lt_of_lt 📖	—	Preorder.toLT DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso	—	—	OrderIso.lt_iff_lt

---

← Back to Index