LogicalEquivalence

📁 Source: Cslib/Foundations/Logic/LogicalEquivalence.lean

Statistics

Metric	Count
Definitions LogicalEquivalence, eqv, eqv_fill_valid, «term_≡_»	4
Theorems congruence	1
Total	5

Cslib.Logic

Definitions

Name	Category	Theorems
LogicalEquivalence 📖	CompData	—
«term_≡_» 📖	CompOp	—

Cslib.Logic.LogicalEquivalence

Definitions

Name	Category	Theorems
eqv 📖	MathDef	1 math math: congruence
eqv_fill_valid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congruence 📖	mathematical	—	Cslib.Congruence eqv	—	—

---

← Back to Index