proposition: Lemma BishopCompact_Compact_BishopCompact : forall (P:Complete X->Prop) (HP:CompactSubset _ P) x, P x <-> inCompact x (BishopCompactAsCompact HP).
proof: Proof. intros P HP x. split. apply BishopCompact_Compact_BishopCompact1. apply BishopCompact_Compact_BishopCompact2. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround