Universe u v w. Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := .
Inductive FiniteT : Type -> Prop :=
| add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T)
| bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X ->
invertible f -> FiniteT Y.
Set Printing Universes.
Axiom a : False. (* Constraint v <= u. Constraint v <= w.
*) Lemma finite_subtype: forall (X:Type) (P:X->Prop),
FiniteT X -> (forall x:X, P x \/ ~ P x) ->
FiniteT {x:X | P x}. Proof. intros. induction H.
destruct (H0 None). elim a.
pose (g := fun (x:{x:T | P (Some x)}) => match x return {x:option T | P x} with
| exist _ x0 i => exist (fun x:option T => P x) (Some x0) i end). apply bij_finite with _ g. apply IHFiniteT. intro; apply H0. elim a.
pose (g := fun (x:{x:X | P (f x)}) => match x with
| exist _ x0 i => exist (fun x:Y => P x) (f x0) i end). apply bij_finite with _ g. apply IHFiniteT. intro; apply H0. elim a.
Qed.
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.6Bemerkung:
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
