Cardinality

📁 Source: Mathlib/Topology/Algebra/Module/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems dense_compl, cardinal_eq_of_isOpen, cardinal_eq_of_mem_nhds, cardinal_eq_of_mem_nhds_zero, continuum_le_cardinal_of_isOpen, continuum_le_cardinal_of_module, continuum_le_cardinal_of_nontriviallyNormedField	7
Total	7

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_compl 📖	mathematical	—	Dense Compl.compl Set Set.instCompl	—	interior_eq_empty_iff_dense_compl lt_irrefl Cardinal.aleph0_lt_continuum continuum_le_cardinal_of_isOpen isOpen_interior Set.notMem_singleton_empty Cardinal.mk_le_mk_of_subset interior_subset le_aleph0

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinal_eq_of_isOpen 📖	mathematical	IsOpen Set.Nonempty	Set.Elem	—	cardinal_eq_of_mem_nhds IsOpen.mem_nhds
cardinal_eq_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Elem	—	ContinuousAt.preimage_mem_nhds Continuous.continuousAt Homeomorph.continuous add_zero cardinal_eq_of_mem_nhds_zero Cardinal.mk_subtype_of_equiv
cardinal_eq_of_mem_nhds_zero 📖	mathematical	Set Filter Filter.instMembership nhds	Set.Elem	—	NormedField.exists_lt_norm pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass lt_irrefl LT.lt.trans norm_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing tendsto_pow_atTop_nhds_zero_of_norm_lt_one norm_inv inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Filter.Tendsto.smul_const Filter.mp_mem zero_smul Filter.univ_mem' Set.mem_smul_set_iff_inv_smul_mem₀ Set.smul_mem_smul_set smul_smul mul_inv_cancel₀ one_smul Subtype.coe_eta inv_mul_cancel₀ Cardinal.mk_congr Cardinal.mk_of_countable_eventually_mem instCountableNat Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
continuum_le_cardinal_of_isOpen 📖	mathematical	IsOpen Set.Nonempty	Cardinal Cardinal.instLE Cardinal.continuum Set.Elem	—	cardinal_eq_of_isOpen continuum_le_cardinal_of_module
continuum_le_cardinal_of_module 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.continuum	—	Cardinal.lift_continuum continuum_le_cardinal_of_nontriviallyNormedField LE.le.trans Cardinal.mk_le_of_module Field.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
continuum_le_cardinal_of_nontriviallyNormedField 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.continuum	—	Perfect.exists_nat_bool_injection isClosed_univ preperfect_iff_nhds NormedField.exists_norm_lt_one Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tendsto_const_nhds tendsto_pow_atTop_nhds_zero_of_norm_lt_one Filter.tendsto_def add_zero Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Set.inter_univ AddLeftCancelSemigroup.toIsLeftCancelAdd pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Set.univ_nonempty Nontrivial.to_nonempty IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Nat.instAtLeastTwoHAddOfNat Cardinal.mk_pi Cardinal.mk_fintype Cardinal.prod_const Cardinal.lift_id Cardinal.mk_eq_aleph0 instCountableNat instInfiniteNat Cardinal.lift_continuum Cardinal.lift_uzero Cardinal.lift_mk_le_lift_mk_of_injective

---

← Back to Index