Lemmas

📁 Source: Mathlib/Logic/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems heq, eq, exists, forall, dite_dite_distrib_left, dite_dite_distrib_right, dite_ite_distrib_left, dite_ite_distrib_right, iff_assoc, iff_left_comm, iff_right_comm, ite_dite_distrib_left, ite_dite_distrib_right, ite_ite_distrib_left, ite_ite_distrib_right	15
Total	15

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
heq 📖	—	—	—	—	—

HEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	—	—	—	—	—

Prop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	—	—	—	—	em
forall 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dite_dite_distrib_left 📖	—	—	—	—	—
dite_dite_distrib_right 📖	—	—	—	—	—
dite_ite_distrib_left 📖	—	—	—	—	dite_dite_distrib_left
dite_ite_distrib_right 📖	—	—	—	—	dite_dite_distrib_right
iff_assoc 📖	—	—	—	—	—
iff_left_comm 📖	—	—	—	—	—
iff_right_comm 📖	—	—	—	—	—
ite_dite_distrib_left 📖	—	—	—	—	dite_dite_distrib_left
ite_dite_distrib_right 📖	—	—	—	—	dite_dite_distrib_right
ite_ite_distrib_left 📖	—	—	—	—	dite_dite_distrib_left
ite_ite_distrib_right 📖	—	—	—	—	dite_dite_distrib_right

---

← Back to Index