Logic in Lean¶

Logical Connectives¶

Conjunction¶

Disjunction¶

Falsehood and Negation¶

Truth¶

Logical Equivalence¶

Existential Quantification¶

Programming with Propositions¶

Applying Theorems to Arguments¶

Lean vs. Set Theory¶

Functional Extensionality¶

Propositions and Booleans¶

Classical vs. Constructive Logic¶