Basic

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

Statistics

Metric	Count
Definitions	0
Theorems instCountable, countable, uncountable, instCountable, instUncountable, countable, uncountable, uncountable_inl, uncountable_inr, instCountable, instUncountable, instCountable, instUncountable, countable_iff_nonempty_embedding, countable_left_of_prod_of_nonempty, countable_prod_swap, countable_right_of_prod_of_nonempty, instCountableForallOfFinite, instCountableInt, instCountablePProd, instCountablePSigma, instCountablePSum, instCountableProd, instCountableSigma, instCountableSum, instUncountableProdOfNonempty, instUncountableProdOfNonempty_1, instUncountableSigmaOfNonempty, nonempty_embedding_nat, uncountable_iff_isEmpty_embedding, untopD_coe_enat	31
Total	31

ENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountable 📖	mathematical	—	Countable ENat	—	Option.instCountable instCountableNat

Function.Embedding

Theorems

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

Option

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountable 📖	mathematical	—	Countable	—	Countable.of_equiv instCountableSum instCountablePUnit
instUncountable 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable

SetCoe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable 📖	mathematical	—	Countable Set.Elem	—	Subtype.countable

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uncountable 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable sigma_mk_injective

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uncountable_inl 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable inl_injective
uncountable_inr 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable inr_injective

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountable 📖	mathematical	—	Countable WithBot	—	Option.instCountable
instUncountable 📖	mathematical	—	Uncountable WithBot	—	Option.instUncountable

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountable 📖	mathematical	—	Countable WithTop	—	Option.instCountable
instUncountable 📖	mathematical	—	Uncountable WithTop	—	Option.instUncountable

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_iff_nonempty_embedding 📖	mathematical	—	Countable Function.Embedding	—	Function.Embedding.inj'
countable_left_of_prod_of_nonempty 📖	mathematical	—	Countable	—	Mathlib.Tactic.Contrapose.contrapose₁ instUncountableProdOfNonempty
countable_prod_swap 📖	mathematical	—	Countable	—	Countable.of_equiv
countable_right_of_prod_of_nonempty 📖	mathematical	—	Countable	—	Mathlib.Tactic.Contrapose.contrapose₁ instUncountableProdOfNonempty_1
instCountableForallOfFinite 📖	—	Countable	—	—	Subsingleton.to_countable Unique.instSubsingleton Fin.isEmpty' Countable.of_equiv instCountableProd instCountableNat Finite.exists_equiv_fin nonempty_embedding_nat Function.Embedding.countable
instCountableInt 📖	mathematical	—	Countable	—	Countable.of_equiv instCountableNat
instCountablePProd 📖	mathematical	—	Countable	—	Countable.of_equiv instCountableProd instCountablePLift
instCountablePSigma 📖	—	Countable	—	—	Countable.of_equiv instCountableSigma instCountablePLift
instCountablePSum 📖	mathematical	—	Countable	—	Countable.of_equiv instCountableSum instCountablePLift
instCountableProd 📖	mathematical	—	Countable	—	Countable.exists_injective_nat Function.Injective.countable instCountableNat Equiv.injective Function.Injective.prodMap
instCountableSigma 📖	—	Countable	—	—	Countable.exists_injective_nat Function.Injective.countable instCountableProd instCountableNat Equiv.injective Function.Injective.sigma_map
instCountableSum 📖	mathematical	—	Countable	—	Countable.exists_injective_nat Function.Injective.countable instCountableNat Equiv.injective Function.Injective.sumMap
instUncountableProdOfNonempty 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable Prod.mk_left_injective
instUncountableProdOfNonempty_1 📖	mathematical	—	Uncountable	—	Function.Injective.uncountable Prod.mk_right_injective
instUncountableSigmaOfNonempty 📖	—	Uncountable	—	—	Sigma.uncountable
nonempty_embedding_nat 📖	mathematical	—	Function.Embedding	—	countable_iff_nonempty_embedding
uncountable_iff_isEmpty_embedding 📖	mathematical	—	Uncountable IsEmpty Function.Embedding	—	not_countable_iff countable_iff_nonempty_embedding not_nonempty_iff
untopD_coe_enat 📖	mathematical	—	WithTop.untopD ENat ENat.instNatCast	—	—

---

← Back to Index