---

Step * of Lemma fset-union-closed

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[fs:(T ⟶ T) List]. ∀[as,bs:fset(T)].
  ((as ⋃ bs closed under fs)) supposing ((bs closed under fs) and (as closed under fs))
BY
{ (RepUR ``fset-closed`` 0 THEN Auto THEN All (RWO "l_all_iff") THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. fs : (T ⟶ T) List
4. as : fset(T)
5. bs : fset(T)
6. ∀f:T ⟶ T. ((f ∈ fs) ⇒ (∀x:T. f x ∈ as supposing x ∈ as))
7. ∀f:T ⟶ T. ((f ∈ fs) ⇒ (∀x:T. f x ∈ bs supposing x ∈ bs))
8. f : T ⟶ T@i
9. (f ∈ fs)@i
10. x : T@i
11. x ∈ as ⋃ bs
⊢ f x ∈ as ⋃ bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[fs:(T  {}\mrightarrow{}  T)  List].  \mforall{}[as,bs:fset(T)].
    ((as  \mcup{}  bs  closed  under  fs))  supposing  ((bs  closed  under  fs)  and  (as  closed  under  fs))


By

---

Latex:
(RepUR  ``fset-closed``  0  THEN  Auto  THEN  All  (RWO  "l\_all\_iff")  THEN  Auto)

---

Home Index