Mathlib Map

Theorems · Definition

Set.SeparatesPoints

{α : Type u_3} → {β : Type u_4} → Set (α → β) → Prop

A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.

Defined in
Mathlib.Logic.Function.Basic
Cited by
4 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Subalgebra.SeparatesPoints · cited by 18Subalgebra.SeparatesPointsseparatesPoints_continuous_of_t35Space_Icc · cited by 1separatesPoints_continuou…separatesPoints_continuous_of_t35Space · cited by 0separatesPoints_continuou…Set.separatesPoints_mono · cited by 0Set.separatesPoints_monoSet.separatesPoints_lipschitzWith_one · cited by 0Set.separatesPoints_lipsc…Set · cited by 53352SetSet.SeparatesPointsCITED BYCITES

Cites1

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

  • Setstatement and proof · cited by 53,352

Cited by5

Results whose statement or proof uses this declaration.