Step
*
of Lemma
continuous'-monotone-bunion
∀[F,G:Type ⟶ Type].
(continuous'-monotone{i:l}(T.F[T] ⋃ G[T])) supposing
(continuous'-monotone{i:l}(T.G[T]) and
continuous'-monotone{i:l}(T.F[T]))
BY
{ (RepUR ``so_apply continuous\'-monotone`` 0 THEN Auto THEN All UnfoldTopAb THEN Auto THEN D 0 THEN Auto) }
1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. ∀[A,B:Type]. (F A) ⊆r (F B) supposing A ⊆r B
4. ∀[X:type-incr-chain{i:l}()]. ((F ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(F (X n)))
5. ∀[A,B:Type]. (G A) ⊆r (G B) supposing A ⊆r B
6. ∀[X:type-incr-chain{i:l}()]. ((G ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(G (X n)))
7. ∀[A,B:Type]. ((F A) ⋃ (G A)) ⊆r ((F B) ⋃ (G B)) supposing A ⊆r B
8. X : type-incr-chain{i:l}()
9. x : (F ⋃n:ℕ.(X n)) ⋃ (G ⋃n:ℕ.(X n))@i
⊢ x ∈ ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))
Latex:
Latex:
\mforall{}[F,G:Type {}\mrightarrow{} Type].
(continuous'-monotone\{i:l\}(T.F[T] \mcup{} G[T])) supposing
(continuous'-monotone\{i:l\}(T.G[T]) and
continuous'-monotone\{i:l\}(T.F[T]))
By
Latex:
(RepUR ``so\_apply continuous\mbackslash{}'-monotone`` 0
THEN Auto
THEN All UnfoldTopAb
THEN Auto
THEN D 0
THEN Auto)
Home
Index