comp163examples-lean

This repository contains examples and exercises in Lean 4 for COMP 163, the discrete structures (mathematics) course at Loyola University Chicago.

Usage

Open the .lean files in your preferred editor with Lean support (VS Code recommended) to explore and run the examples.

Alternatively, use the Lean 4 Web links in the index below to try them in the Lean 4 Web playground. This option doesn't require any installation.

Examples

Example	Source	Try in Lean 4 Web
Basic set example	basic/basic1.lean	Open in Lean 4 Web
Basic examples (min/max commutativity)	basic/basic2.lean	Open in Lean 4 Web
W7p7 - Algebra example 1	w7p7-algebra/algebra1.lean	Open in Lean 4 Web
W7p7 - Algebra example 2	w7p7-algebra/algebra2.lean	Open in Lean 4 Web
W7p7 - Algebra example 3	w7p7-algebra/algebra3.lean	Open in Lean 4 Web
W7p10 - Sets example 1	w7p10-sets/sets1.lean	Open in Lean 4 Web
W7p10 - Sets example 2	w7p10-sets/sets2.lean	Open in Lean 4 Web
W7p10 - Sets example 3	w7p10-sets/sets3.lean	Open in Lean 4 Web
W7p12 - Contradiction example 1	w7p12-contradiction/contradiction1.lean	Open in Lean 4 Web
W7p12 - Contradiction example 2	w7p12-contradiction/contradiction2.lean	Open in Lean 4 Web
W7p12 - Contradiction example 3 (TODO)	w7p12-contradiction/contradiction3.lean	Open in Lean 4 Web
W7p10 - Sets example 1 (by contradiction)	w7p12-contradiction/sets1contradiction.lean	Open in Lean 4 Web
W7p10 - Sets example 2 (by contradiction)	w7p12-contradiction/sets2contradiction.lean	Open in Lean 4 Web
W7p14 - Contrapositive example 1 (TODO)	w7p14-contrapositive/contrapositive1.lean	Open in Lean 4 Web
W7p14 - Contrapositive example 2	w7p14-contrapositive/contrapositive2.lean	Open in Lean 4 Web
W7p14 - Contrapositive example 3	w7p14-contrapositive/contrapositive3.lean	Open in Lean 4 Web
W7p14 - Contrapositive example 4	w7p14-contrapositive/contrapositive4.lean	Open in Lean 4 Web