✳flâneur — a map of the web's best reading

3. Logic — Mathematics in Lean v4.19.0 documentation

leanprover-community.github.io · 13,572 words · saved by 1 readers

In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like “ 𝑥 divides 𝑦 .” Complex mathematical statements are built up from simple ones like these using logical terms like “and,” “or,” “not,” and “if … then,” “every,” and “some.” In this chapter, we show you how to work with statements that are built up in this way. Consider the statement after the #check: In words, we would say “for every real number x, if 0 ≤ x then the absolute value of x equals x”. We can also have more complicated statements like: In words, we would say “for every x, y, and ε, if 0 < ε ≤ 1, the absolute value of x is less than ε, and the absolute value of y is less than ε, then the absolute value of x * y is less than ε.” In Lean, in a sequence of implications there are implicit parentheses grouped to the right. So the expression above means “if 0 < ε then if ε ≤ 1 then if |x| < ε …” As a result, the expression says that all the assumptions together imply the conclusio

3. Logic - Mathematics in Lean v4.19.0 documentation 3. Logic View page source 3. Logic  In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like “ \(x\) divides \(y\) .” Complex mathematical statements are built up from simple ones like these using logical terms like “and,” “or,” “not,” and “if … then,” “every,” and “some.” In this chapter, we show you how to work with statements that are built up in this way. 3.1. Implication and the Universal Quantifier

Explore this link on the map →

saved by

Janabel Xia

3. Logic — Mathematics in Lean v4.19.0 documentation

saved by

related reading