CompleteMetrizable

Statistics

Metric	Count
Definitions	0
Theorems `of_completelyPseudoMetrizable`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`of_completelyPseudoMetrizable` 📖	mathematical	—	`BaireSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.div_pos` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero` `ENNReal.pow_ne_top` `ENNReal.ofNat_ne_top` `EMetric.mem_closure_iff` `ENNReal.half_pos` `Filter.HasBasis.mem_iff` `Metric.nhds_basis_closedEBall` `isOpen_iff_mem_nhds` `lt_min` `min_le_right` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_of_lt` `PseudoEMetricSpace.edist_comm` `le_trans` `min_le_left` `le_rfl` `ENNReal.add_halves` `mem_closure_iff_nhds_basis` `LT.lt.ne'` `Metric.mem_closedEBall_self` `Set.Subset.trans` `Set.inter_subset_left` `Metric.closedEBall_subset_closedEBall` `cauchySeq_of_edist_le_geometric_two` `ENNReal.one_ne_top` `cauchySeq_tendsto_of_complete` `TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace` `Nat.le_induction` `Set.Subset.refl` `IsClosed.mem_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Metric.isClosed_closedEBall` `Filter.Eventually.mono` `Filter.eventually_ge_atTop` `Set.inter_subset_right` `Function.sometimes_spec`

---