Step
*
of Lemma
dMpair-eq-meet
∀[I:fset(ℕ)]. ∀[i,j:ℕ].  (dMpair(i;j) = <i> ∧ <j> ∈ Point(dM(I))) supposing (j ∈ I and i ∈ I)
BY
{ Intros }
1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
⊢ dMpair(i;j) = <i> ∧ <j> ∈ Point(dM(I))
Latex:
Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].    (dMpair(i;j)  =  <i>  \mwedge{}  <j>)  supposing  (j  \mmember{}  I  and  i  \mmember{}  I)
By
Latex:
Intros
Home
Index