Step * of Lemma u-almost-full-filter

`∀A,B:ℕ ⟶ ℙ.`
`  ((u-almost-full(n.A[n]) `` u-almost-full(n.B[n]) `` u-almost-full(n.A[n] ∧ B[n]))`
`  ∧ ((∀n:ℕ. (A[n] `` B[n])) `` u-almost-full(n.A[n]) `` u-almost-full(n.B[n]))`
`  ∧ u-almost-full(n.True))`
BY
`{ Auto }`

1
`1. A : ℕ ⟶ ℙ@i'`
`2. B : ℕ ⟶ ℙ@i'`
`3. u-almost-full(n.A[n])@i`
`4. u-almost-full(n.B[n])@i`
`⊢ u-almost-full(n.A[n] ∧ B[n])`

2
`1. A : ℕ ⟶ ℙ@i'`
`2. B : ℕ ⟶ ℙ@i'`
`3. ∀n:ℕ. (A[n] `` B[n])@i`
`4. u-almost-full(n.A[n])@i`
`5. u-almost-full(n.B[n]) `` u-almost-full(n.A[n] ∧ B[n])`
`⊢ u-almost-full(n.B[n])`

3
`1. A : ℕ ⟶ ℙ@i'`
`2. B : ℕ ⟶ ℙ@i'`
`3. u-almost-full(n.A[n]) `` u-almost-full(n.B[n]) `` u-almost-full(n.A[n] ∧ B[n])`
`4. (∀n:ℕ. (A[n] `` B[n])) `` u-almost-full(n.A[n]) `` u-almost-full(n.B[n])`
`⊢ u-almost-full(n.True)`

Latex:

Latex:
\mforall{}A,B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
((u-almost-full(n.A[n])  {}\mRightarrow{}  u-almost-full(n.B[n])  {}\mRightarrow{}  u-almost-full(n.A[n]  \mwedge{}  B[n]))
\mwedge{}  ((\mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  B[n]))  {}\mRightarrow{}  u-almost-full(n.A[n])  {}\mRightarrow{}  u-almost-full(n.B[n]))
\mwedge{}  u-almost-full(n.True))

By

Latex:
Auto

Home Index