---

Step * of Lemma fiber-discrete-equal

No Annotations
∀[B:Type]. ∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ discr(B))}]. ∀[z:{X ⊢ _:discr(B)}]. ∀[fbr:{X ⊢ _:Fiber(f;z)}].
  (app(f; fiber-member(fbr)) = z ∈ {X ⊢ _:discr(B)})
BY
{ (Intros
   THEN (InstLemma `fiber-path_wf` [⌜X⌝;⌜A⌝;⌜discr(B)⌝;⌜f⌝;⌜z⌝;⌜fbr⌝]⋅ THENA Auto)
   THEN InstLemma `discrete-path-endpoints`
    [⌜X⌝;⌜B⌝;⌜z⌝;⌜app(f; fiber-member(fbr))⌝;fiber-path(fbr)]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[B:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  discr(B))\}].  \mforall{}[z:\{X  \mvdash{}  \_:discr(B)\}].
\mforall{}[fbr:\{X  \mvdash{}  \_:Fiber(f;z)\}].
    (app(f;  fiber-member(fbr))  =  z)


By

---

Latex:
(Intros
  THEN  (InstLemma  `fiber-path\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}discr(B)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}fbr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `discrete-path-endpoints`
    [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}app(f;  fiber-member(fbr))\mkleeneclose{};fiber-path(fbr)]\mcdot{}
  THEN  Auto)

---

Home Index