Defs

📁 Source: Mathlib/Data/Countable/Defs.lean

Statistics

Metric	Count
Definitions Uncountable	1
Theorems countable, exists_injective_nat, exists_injective_nat', of_equiv, countable_iff, uncountable_iff, to_countable, countable, uncountable, countable, uncountable, countable, countable', countable, to_countable, countable, not_countable, of_equiv, countable_iff_exists_injective, countable_iff_exists_surjective, exists_surjective_nat, instCountableFin, instCountableNat, instCountablePLift, instCountablePUnit, instCountableQuotient, instCountableULift, instInfiniteOfUncountable, instUncountablePLift, instUncountableULift, not_countable, not_countable_iff, not_injective_uncountable_countable, not_surjective_countable_uncountable, not_uncountable, not_uncountable_iff, uncountable_iff_forall_not_surjective, uncountable_iff_not_countable	38
Total	39

Bool

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	injective_iff

Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_injective_nat 📖	—	—	—	—	exists_injective_nat'
exists_injective_nat' 📖	—	—	—	—	—
of_equiv 📖	mathematical	—	Countable	—	Function.Injective.countable Equiv.injective

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_iff 📖	mathematical	—	Countable	—	Countable.of_equiv
uncountable_iff 📖	mathematical	—	Uncountable	—	Uncountable.of_equiv

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_countable 📖	mathematical	—	Countable	—	exists_equiv_fin Countable.of_equiv instCountableFin

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Countable.exists_injective_nat
uncountable 📖	mathematical	—	Uncountable	—	not_countable countable

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Function.Injective.countable Function.injective_surjInv
uncountable 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable Function.injective_surjInv

Prop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Subsingleton.to_countable
countable' 📖	mathematical	—	Countable	—	Countable.of_equiv Bool.countable

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Function.Surjective.countable Quot.mk_surjective

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_countable 📖	mathematical	—	Countable	—	—

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable	—	Function.Injective.countable val_injective

Uncountable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_countable 📖	mathematical	—	Countable	—	—
of_equiv 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable Equiv.injective

(root)

Definitions

Name	Category	Theorems
Uncountable 📖	CompData	28 math math: Function.Injective.uncountable, Function.Embedding.uncountable, not_uncountable_iff, Set.not_countable_univ_iff, instUncountableProdOfNonempty_1, WithBot.instUncountable, instUncountablePLift, Nimber.uncountable, Cardinal.uncountable, WithTop.instUncountable, Cardinal.aleph0_lt_mk_iff, not_uncountable, Sum.uncountable_inl, Uncountable.of_not_small, uncountable_iff_not_countable, uncountable_iff_isEmpty_embedding, Function.Surjective.uncountable, Equiv.uncountable_iff, instUncountableULift, Cardinal.instUncountableReal, Uncountable.of_equiv, not_countable_iff, instUncountableProdOfNonempty, uncountable_iff_forall_not_surjective, Sigma.uncountable, Ordinal.uncountable, Option.instUncountable, Sum.uncountable_inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_iff_exists_injective 📖	mathematical	—	Countable	—	—
countable_iff_exists_surjective 📖	mathematical	—	Countable	—	exists_surjective_nat Function.Surjective.countable instCountableNat
exists_surjective_nat 📖	—	—	—	—	Countable.exists_injective_nat Function.invFun_surjective
instCountableFin 📖	mathematical	—	Countable	—	Function.Injective.countable instCountableNat
instCountableNat 📖	mathematical	—	Countable	—	—
instCountablePLift 📖	mathematical	—	Countable	—	Function.Injective.countable Equiv.injective
instCountablePUnit 📖	mathematical	—	Countable	—	Subsingleton.to_countable
instCountableQuotient 📖	mathematical	—	Countable	—	Quotient.countable
instCountableULift 📖	mathematical	—	Countable	—	Countable.of_equiv
instInfiniteOfUncountable 📖	mathematical	—	Infinite	—	not_countable Finite.to_countable
instUncountablePLift 📖	mathematical	—	Uncountable	—	Uncountable.of_equiv
instUncountableULift 📖	mathematical	—	Uncountable	—	Uncountable.of_equiv
not_countable 📖	mathematical	—	Countable	—	Uncountable.not_countable
not_countable_iff 📖	mathematical	—	Countable Uncountable	—	uncountable_iff_not_countable
not_injective_uncountable_countable 📖	—	—	—	—	not_countable Function.Injective.countable
not_surjective_countable_uncountable 📖	—	—	—	—	not_countable Function.Surjective.countable
not_uncountable 📖	mathematical	—	Uncountable	—	not_uncountable_iff
not_uncountable_iff 📖	mathematical	—	Uncountable Countable	—	uncountable_iff_not_countable
uncountable_iff_forall_not_surjective 📖	mathematical	—	Uncountable	—	not_countable_iff countable_iff_exists_surjective
uncountable_iff_not_countable 📖	mathematical	—	Uncountable Countable	—	—

---

← Back to Index