---

Step * of Lemma discrete-fun-invariant

∀[A,B:Type]. ∀[f:{() ⊢ _:(discr(A) ⟶ discr(B))}]. ∀[I:fset(ℕ)]. ∀[a:()(I)].
  ((f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a))
BY
{ (InstLemma `discrete-fun-at` [] THEN RepeatFor 3 (ParallelLast') THEN Intros) }

1
1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. ∀[I:fset(ℕ)]. ∀[a:()(I)].  ((f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a))
5. I : fset(ℕ)
6. a : ()(I)
⊢ (f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:\{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:()(I)].    ((f  I  a)  =  (f  \{\}  \mcdot{}))


By

---

Latex:
(InstLemma  `discrete-fun-at`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Intros)

---

Home Index