---

Step * of Lemma fset-image_functionality_wrt_subset

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s1,s2:fset(T)].  f"(s1) ⊆ f"(s2) supposing s1 ⊆ s2
BY
{ ((Auto THEN ParallelLast) THEN Auto) }

1
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. f : T ⟶ A
6. s1 : fset(T)
7. s2 : fset(T)
8. ∀a:T. a ∈ s2 supposing a ∈ s1
9. a : A
10. a ∈ f"(s1)
⊢ a ∈ f"(s2)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[s1,s2:fset(T)].
    f"(s1)  \msubseteq{}  f"(s2)  supposing  s1  \msubseteq{}  s2


By

---

Latex:
((Auto  THEN  ParallelLast)  THEN  Auto)

---

Home Index