Skip to main content
MathOverflow

Return to Question

added 24 characters in body
Source Link
Emanuele Paolini
Emanuele Paolini
  • 702
  • 3
  • 11

I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

Definition (rational numbers) Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given by $$ (q,p) \sim (q',p') \iff pq' = p'q. $$ We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. On $\mathbb Q$ we define addition and multiplication as follows $$ [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\ [(q,p)] \cdot[(q',p')] = [(qq',pp')] $$ With these operations and choosing $0=[(1,0)]$$0_\mathbb Q=[(1,0)]$, and $1=[(1,1)]$$1_\mathbb Q=[(1,1)]$ turns out that $\mathbb Q$ is a field.

Proof. We are going to prove that $\sim$ is indeed an equivalence relation, that addition and multiplication are well defined and that the resulting set is a field. [...]

I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

Definition (rational numbers) Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given by $$ (q,p) \sim (q',p') \iff pq' = p'q. $$ We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. On $\mathbb Q$ we define addition and multiplication as follows $$ [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\ [(q,p)] \cdot[(q',p')] = [(qq',pp')] $$ With these operations and choosing $0=[(1,0)]$, $1=[(1,1)]$ turns out that $\mathbb Q$ is a field.

Proof. We are going to prove that $\sim$ is indeed an equivalence relation, that addition and multiplication are well defined and that the resulting set is a field. [...]

I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

Definition (rational numbers) Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given by $$ (q,p) \sim (q',p') \iff pq' = p'q. $$ We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. On $\mathbb Q$ we define addition and multiplication as follows $$ [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\ [(q,p)] \cdot[(q',p')] = [(qq',pp')] $$ With these operations and choosing $0_\mathbb Q=[(1,0)]$, and $1_\mathbb Q=[(1,1)]$ turns out that $\mathbb Q$ is a field.

Proof. We are going to prove that $\sim$ is indeed an equivalence relation, that addition and multiplication are well defined and that the resulting set is a field. [...]

Source Link
Emanuele Paolini
Emanuele Paolini
  • 702
  • 3
  • 11

mixing theorem with definition (definition with proof)

I often find myself writing a definition which requires a proof. You are defining a term and, contextually, need to prove that the definition makes sense.

How can you express that? What about a definition with a proof?

Sometime one can write the definition and then the theorem. But often happens that many definition which should stay together need to be split because a theorem is required in between.

A tentative example:

Definition (rational numbers) Let $\sim$ be the equivalence relation on $\mathbb Z^*\times \mathbb Z$ given by $$ (q,p) \sim (q',p') \iff pq' = p'q. $$ We define $\mathbb Q= (\mathbb Z^*\times \mathbb Z)/\sim$. On $\mathbb Q$ we define addition and multiplication as follows $$ [(q,p)] + [(q',p')] = [(qq',pq'+p'q)] \\ [(q,p)] \cdot[(q',p')] = [(qq',pp')] $$ With these operations and choosing $0=[(1,0)]$, $1=[(1,1)]$ turns out that $\mathbb Q$ is a field.

Proof. We are going to prove that $\sim$ is indeed an equivalence relation, that addition and multiplication are well defined and that the resulting set is a field. [...]