Mathlib Map

Theorems · Theorem · general topology

CantorScheme.Disjoint.map_injective

∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α},
  CantorScheme.Disjoint A → Function.Injective (CantorScheme.inducedMap A).snd

A scheme where the children of each set are pairwise disjoint induces an injective map.

Defined in
Mathlib.Topology.MetricSpace.CantorScheme
Cited by
1 results in Mathlib
Foundations
Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Perfect.exists_nat_bool_injection · cited by 2Perfect.exists_nat_bool_i…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemSet.not_disjoint_iff · cited by 30Set.not_disjoint_iffPiNat.res · cited by 12PiNat.resCantorScheme.inducedMap · cited by 5CantorScheme.inducedMapCantorScheme.map_mem · cited by 3CantorScheme.map_memCantorScheme.Disjoint · cited by 2CantorScheme.DisjointPiNat.res_injective · cited by 1PiNat.res_injectivePiNat.res_succ · cited by 1PiNat.res_succDisjoint.map_injectiveCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.