Step * of Lemma rleq-iff-all-rless

[x,y:ℝ].  uiff(x ≤ y;∀e:{e:ℝr0 < e} (x ≤ (y e)))
BY
Auto }

1
1. : ℝ
2. : ℝ
3. x ≤ y
4. {e:ℝr0 < e} 
⊢ x ≤ (y e)

2
1. : ℝ
2. : ℝ
3. ∀e:{e:ℝr0 < e} (x ≤ (y e))
⊢ x ≤ y


Latex:


Latex:
\mforall{}[x,y:\mBbbR{}].    uiff(x  \mleq{}  y;\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  (x  \mleq{}  (y  +  e)))


By


Latex:
Auto




Home Index