part1/Relations: Fix Typo
"form `m ≤ n`" -> "from `m ≤ n`"
This commit is contained in:
parent
69da80df93
commit
aaf5b914b0
1 changed files with 1 additions and 1 deletions
|
@ -161,7 +161,7 @@ Chapter [Decidable]({{ site.baseurl }}/Decidable/).
|
|||
## Inversion
|
||||
|
||||
In our defintions, we go from smaller things to larger things.
|
||||
For instance, form `m ≤ n` we can conclude `suc m ≤ suc n`,
|
||||
For instance, from `m ≤ n` we can conclude `suc m ≤ suc n`,
|
||||
where `suc m` is bigger than `m` (that is, the former contains
|
||||
the latter), and `suc n` is bigger than `n`. But sometimes we
|
||||
want to go from bigger things to smaller things.
|
||||
|
|
Loading…
Add table
Reference in a new issue