Paracompact

📁 Source: Mathlib/Topology/EMetricSpace/Paracompact.lean

Statistics

Metric	Count
Definitions	0
Theorems t4Space, instParacompactSpace, t4Space	3
Total	3

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t4Space 📖	mathematical	—	T4Space UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	Metric.t4Space

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instParacompactSpace 📖	mathematical	—	ParacompactSpace UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	Nat.instAtLeastTwoHAddOfNat ENNReal.pow_pos ENNReal.inv_pos ENNReal.ofNat_ne_top pow_le_pow_right_of_le_one' IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.inv_le_one LT.lt.le ENNReal.one_lt_two pow_succ' ENNReal.mul_inv_cancel two_ne_zero ZeroLEOneClass.neZero.two IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.one IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid one_mul exists_wellOrder wellFounded_lt WellFounded.min_mem WellFounded.not_lt_min Set.iUnion_congr_Prop Nat.strongRecOn'_beta EMetric.isOpen_iff ENNReal.div_pos_iff LT.lt.ne' GT.gt.lt ENNReal.coe_ne_top ENNReal.exists_inv_two_pow_lt Set.Subset.trans eball_subset_eball mul_comm ENNReal.mul_lt_of_lt_div mem_eball_self isOpen_iUnion isOpen_eball LT.lt.trans_le le_mul_of_one_le_left' covariant_swap_mul_of_covariant_mul Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Set.iUnion_eq_univ_iff IsOpen.mem_nhds Filter.HasBasis.mem_iff nhds_basis_uniformity uniformity_basis_edist_inv_two_pow eball_mem_nhds disjoint_iff_inf_le edist_triangle_left ENNReal.add_lt_add add_le_add covariant_swap_add_of_covariant_add two_mul PseudoEMetricSpace.edist_triangle add_comm mul_le_mul_right add_le_add_right Nat.instIsOrderedAddMonoid le_rfl mul_add Distrib.leftDistribClass two_add_one_eq_three add_mul Distrib.rightDistribClass Ne.lt_or_gt Set.Finite.biUnion' Set.finite_le_nat Set.Subsingleton.finite Set.finite_singleton Set.Finite.subset not_lt Disjoint.le_bot
t4Space 📖	mathematical	—	T4Space UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	—	T4Space.of_paracompactSpace_t2Space T25Space.t2Space T3Space.t25Space instT3Space EMetricSpace.instT0Space UniformSpace.to_regularSpace instParacompactSpace

---

← Back to Index