---

Step * of Lemma fset-constrained-image_functionality_wrt_subset

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[s1,s2:fset(T)].
  f"(s1) s.t. P ⊆ f"(s2) s.t. P 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. P : A ⟶ 𝔹
7. s1 : fset(T)
8. s2 : fset(T)
9. ∀a:T. a ∈ s2 supposing a ∈ s1
10. a : A
11. a ∈ f"(s1) s.t. P
⊢ a ∈ f"(s2) s.t. P

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  ParallelLast)  THEN  Auto)

---

Home Index