Lean for All

Day 5: And, or, not, if and only if🔗

Read ∧, ∨, ¬, ≠ and ↔, and know how they group.

Four more symbols, and you can read most statements:

P ∧ Q: P and Q (both hold).
P ∨ Q: P or Q (at least one holds, maybe both).
¬ P: not P. And a ≠ b is short for ¬ (a = b).
P ↔ Q: P if and only if Q (each implies the other).

theorem facts : 2 < 3 ∧ 3 < 4 := by⊢ 2 < 3 ∧ 3 < 4 decideAll goals completed! 🐙
theorem either : 2 = 3 ∨ 2 = 2 := by⊢ 2 = 3 ∨ 2 = 2 decideAll goals completed! 🐙
theorem nope : ¬ (2 = 3) := by⊢ ¬2 = 3 decideAll goals completed! 🐙

(by decide asks Lean to settle a statement about specific numbers by computing.)

Like × before + in arithmetic, these symbols have an order. From tightest to loosest:

¬ (applies to the smallest piece after it)
=, <, ≤, ≠ (comparisons)
∧
∨
→
↔

So ¬ P ∧ Q means (¬ P) ∧ Q, not ¬ (P ∧ Q). And P ∧ Q → R means (P ∧ Q) → R. When in doubt, look for brackets.

↔ is two arrows in one: P ↔ Q means P → Q and Q → P.

theorem even_iff (n : Nat) : n % 2 = 0 ↔ (n + 2) % 2 = 0 := byn:Nat⊢ n % 2 = 0 ↔ (n + 2) % 2 = 0 omegaAll goals completed! 🐙

A common slip is to treat a one-way → as if it were ↔. When a claim says “exactly when” or “if and only if”, the Lean statement must use ↔.

Now you can read hypotheses that combine conditions:

theorem small (n : Nat) (h : n > 2 ∧ n < 5) : n = 3 ∨ n = 4 := byn:Nath:n > 2 ∧ n < 5⊢ n = 3 ∨ n = 4 omegaAll goals completed! 🐙

For every n, if n > 2 and n < 5, then n = 3 or n = 4.

Day 5: And, or, not, if and only if🔗

Check yourself🔗