Skip to content

Instantly share code, notes, and snippets.

@JasonGross

JasonGross/pi_limit.v

Created January 2, 2014 19:19
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save JasonGross/8224881 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save JasonGross/8224881 to your computer and use it in GitHub Desktop.
Download ZIP
pi is limit
Raw
pi_limit.v
Set Implicit Arguments.
Section lim.
Variable J : Type.
Variable F : J -> Type.
Variable L : Type.
Variable Phi : forall x, L -> F x.
Definition IsLimit := forall N (Psi : forall x, N -> F x), { u : N -> L & forall x, (fun y => (Phi x) (u y)) = Psi x }.
End lim.
Lemma PiIsLimit J F : @IsLimit J F (forall x, F x) (fun H f => f H).
intros N Psi.
exists (fun n x => Psi x n).
intro x.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment