RatLemmas

📁 Source: Mathlib/Topology/Instances/RatLemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems cocompact_inf_nhds_neBot, dense_compl_compact, instTotallyDisconnectedSpace, interior_compact_eq_empty, not_countably_generated_cocompact, not_countably_generated_nhds_infty_opc, not_firstCountableTopology_opc, not_secondCountableTopology_opc	8
Total	8

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocompact_inf_nhds_neBot 📖	mathematical	—	Filter.NeBot Filter Filter.instInf Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace nhds	—	Filter.HasBasis.neBot_iff Filter.HasBasis.inf Filter.hasBasis_cocompact nhds_basis_opens Set.inter_comm Dense.inter_open_nonempty dense_compl_compact
dense_compl_compact 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	Dense Compl.compl Set Set.instCompl	—	interior_eq_empty_iff_dense_compl interior_compact_eq_empty
instTotallyDisconnectedSpace 📖	mathematical	—	TotallyDisconnectedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	exists_irrational_btwn cast_lt Real.instIsStrictOrderedRing IsPreconnected.image Continuous.continuousOn continuous_coe_real Set.OrdConnected.out isPreconnected_iff_ordConnected instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.mem_image_of_mem LT.lt.le Set.image_subset_range Ne.lt_or_gt
interior_compact_eq_empty 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	interior Set Set.instEmptyCollection	—	IsDenseInducing.interior_compact_eq_empty TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsDenseEmbedding.isDenseInducing isDenseEmbedding_coe_real dense_irrational
not_countably_generated_cocompact 📖	mathematical	—	Filter.IsCountablyGenerated Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	Filter.exists_seq_tendsto Filter.Inf.isCountablyGenerated FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace cocompact_inf_nhds_neBot Filter.tendsto_inf Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually IsCompact.compl_mem_cocompact Filter.Tendsto.isCompact_insert_range
not_countably_generated_nhds_infty_opc 📖	mathematical	—	Filter.IsCountablyGenerated OnePoint nhds OnePoint.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace OnePoint.infty	—	Filter.comap.isCountablyGenerated not_countably_generated_cocompact Filter.coclosedCompact_eq_cocompact instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace OnePoint.comap_coe_nhds_infty
not_firstCountableTopology_opc 📖	mathematical	—	FirstCountableTopology OnePoint OnePoint.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	not_countably_generated_nhds_infty_opc FirstCountableTopology.nhds_generated_countable
not_secondCountableTopology_opc 📖	mathematical	—	SecondCountableTopology OnePoint OnePoint.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	not_firstCountableTopology_opc TopologicalSpace.SecondCountableTopology.to_firstCountableTopology

---

← Back to Index