flâneur

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 &#61633; In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like &#8220; \(x\) divides \(y\) .&#8221; Complex mathematical statements are built up from simple ones like these using logical terms like &#8220;and,&#8221; &#8220;or,&#8221; &#8220;not,&#8221; and &#8220;if &#8230; then,&#8221; &#8220;every,&#8221; and &#8220;some.&#8221; 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

saved by

related reading