NatEmbedding

📁 Source: Mathlib/Topology/NatEmbedding.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_infinite_discreteTopology, exists_seq_infinite_isOpen_pairwise_disjoint, exists_topology_isEmbedding_nat	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_infinite_discreteTopology 📖	mathematical	—	Set.Infinite DiscreteTopology Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	exists_topology_isEmbedding_nat Set.infinite_range_of_injective instInfiniteNat Topology.IsEmbedding.injective Topology.IsEmbedding.discreteTopology instDiscreteTopologyNat Homeomorph.isEmbedding
exists_seq_infinite_isOpen_pairwise_disjoint 📖	mathematical	—	Set.Infinite IsOpen Pairwise Function.onFun Set Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Set.singleton_nonempty isOpen_discrete Function.instEmbeddingLikeEmbedding Disjoint.symm exists_seq_of_forall_finset_exists' Filter.inter_mem_inf Filter.biInter_finset_mem interior_mem_nhds Filter.mem_principal_self Filter.NeBot.nonempty_of_mem t2_separation IsOpen.inter isOpen_biInter_finset isOpen_interior Filter.mem_of_superset IsOpen.mem_nhds Set.disjoint_left interior_subset Set.mem_iInter₂ Set.infinite_iUnion instInfiniteNat Pairwise.eq Set.Nonempty.ne_empty isOpen_iUnion Set.disjoint_iUnion_left Set.disjoint_iUnion_right
exists_topology_isEmbedding_nat 📖	mathematical	—	Topology.IsEmbedding instTopologicalSpaceNat	—	exists_seq_infinite_isOpen_pairwise_disjoint Topology.IsInducing.isEmbedding T1Space.t0Space T2Space.t1Space DiscreteTopology.toT2Space instDiscreteTopologyNat eq_bot_of_singletons_open Set.eq_singleton_iff_unique_mem Pairwise.eq Set.not_disjoint_iff Set.Infinite.nonempty

---

← Back to Index