Step
*
of Lemma
continuous-monotone-union
∀F,G:Type ⟶ Type. (ContinuousMonotone(T.F[T])
⇒ ContinuousMonotone(T.G[T])
⇒ ContinuousMonotone(T.F[T] + G[T]))
BY
{ (Unfold `so_apply` 0
THEN Auto
THEN RepeatFor 4 ((D 0 THEN Auto))
THEN DoSubsume
THEN Auto
THEN BackThruSomeHyp'
THEN Auto) }
Latex:
Latex:
\mforall{}F,G:Type {}\mrightarrow{} Type.
(ContinuousMonotone(T.F[T]) {}\mRightarrow{} ContinuousMonotone(T.G[T]) {}\mRightarrow{} ContinuousMonotone(T.F[T] + G[T]))
By
Latex:
(Unfold `so\_apply` 0
THEN Auto
THEN RepeatFor 4 ((D 0 THEN Auto))
THEN DoSubsume
THEN Auto
THEN BackThruSomeHyp'
THEN Auto)
Home
Index