---

Step * of Lemma fset-constrained-image-singleton

∀[eqt,eqa:Top]. ∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[x:T].  (f"({x}) s.t. P ~ if P (f x) then {f x} else {} fi )
BY
{ ((Auto THEN RepUR ``fset-singleton fset-constrained-image f-union fset-union l-union`` 0) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[eqt,eqa:Top].  \mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:T].
    (f"(\{x\})  s.t.  P  \msim{}  if  P  (f  x)  then  \{f  x\}  else  \{\}  fi  )


By

---

Latex:
((Auto  THEN  RepUR  ``fset-singleton  fset-constrained-image  f-union  fset-union  l-union``  0)
  THEN  AutoSplit
  )

---

Home Index