proposition: Proposition is_compact_approximating_family (x : X) (i : compact_approximating_family x) : is_compact_el (compact_approximating_family x i).
proof: Proof. exact (pr12 (AX x) i). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous