Arithmetic

📁 Source: Mathlib/SetTheory/Cardinal/Arithmetic.lean

Statistics

Metric	Count
Definitions	0
Theorems add_ciSup, add_eq_left, add_eq_left_iff, add_eq_max, add_eq_max', add_eq_right, add_eq_right_iff, add_eq_self, add_le_add_iff_of_lt_aleph0, add_le_max, add_le_of_le, add_lt_add, add_lt_add_iff_of_left_lt_aleph0, add_lt_add_iff_of_right_lt_aleph0, add_lt_of_lt, add_mk_eq_max, add_mk_eq_max', add_mk_eq_self, add_nat_eq, add_nat_inj, add_nat_le_add_nat_iff, add_one_eq, add_one_inj, add_one_le_add_one_iff, add_right_inj_of_lt_aleph0, aleph0_mul_aleph, aleph0_mul_eq, aleph0_mul_mk_eq, aleph_add_aleph, aleph_mul_aleph, aleph_mul_aleph0, ciSup_add, ciSup_add_ciSup, ciSup_mul, ciSup_mul_ciSup, eq_of_add_eq_add_left, eq_of_add_eq_add_right, eq_of_add_eq_of_aleph0_le, extend_function, extend_function_finite, extend_function_of_lt, le_mul_left, le_mul_right, mk_add_one_eq, mk_arrow_eq_zero_iff, mk_bounded_set_le, mk_bounded_set_le_of_infinite, mk_bounded_subset_le, mk_compl_eq_mk_compl_finite, mk_compl_eq_mk_compl_finite_lift, mk_compl_eq_mk_compl_finite_same, mk_compl_eq_mk_compl_infinite, mk_compl_finset_of_infinite, mk_compl_of_infinite, mk_embedding_eq_arrow_of_le, mk_embedding_eq_arrow_of_lift_le, mk_embedding_eq_zero_iff_lift_lt, mk_embedding_eq_zero_iff_lt, mk_embedding_le_arrow, mk_equiv_comm, mk_equiv_eq_arrow_of_eq, mk_equiv_eq_arrow_of_lift_eq, mk_equiv_eq_zero_iff_lift_ne, mk_equiv_eq_zero_iff_ne, mk_equiv_le_embedding, mk_equiv_of_eq, mk_equiv_of_lift_eq, mk_finset_of_infinite, mk_list_eq_aleph0, mk_list_eq_max, mk_list_eq_max_mk_aleph0, mk_list_eq_mk, mk_list_le_max, mk_mul_aleph0_eq, mk_perm_eq_self_power, mk_perm_eq_two_power, mk_surjective_eq_arrow_of_le, mk_surjective_eq_arrow_of_lift_le, mk_surjective_eq_zero_iff, mk_surjective_eq_zero_iff_lift, mul_aleph0_eq, mul_ciSup, mul_eq_left, mul_eq_left_iff, mul_eq_max, mul_eq_max', mul_eq_max_of_aleph0_le_left, mul_eq_max_of_aleph0_le_right, mul_eq_right, mul_eq_self, mul_le_max, mul_le_max_of_aleph0_le_left, mul_le_max_of_aleph0_le_right, mul_lt_of_lt, mul_mk_eq_max, mul_natCast_inj, mul_natCast_le_mul_natCast, mul_natCast_lt_mul_natCast, mul_natCast_strictMono, natCast_mul_inj, natCast_mul_le_natCast_mul, natCast_mul_lt_natCast_mul, natCast_mul_strictMono, nat_add_eq, nat_power_eq, pow_eq, pow_le, power_eq_two_power, power_le_aleph0, power_nat_eq, power_nat_le, power_nat_le_max, power_self_eq, powerlt_aleph0, powerlt_aleph0_le, prod_eq_two_power, sum_eq_iSup, sum_eq_iSup_lift, sum_eq_iSup_of_lift_mk_le_iSup, sum_eq_iSup_of_mk_le_iSup, sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, sum_pow_eq_max_aleph0, sum_pow_le_max_aleph0	123
Total	123

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_ciSup 📖	mathematical	BddAbove Cardinal instLE Set.range	instAdd iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	add_comm ciSup_add
add_eq_left 📖	mathematical	Cardinal instLE aleph0	instAdd	—	add_eq_max max_eq_left
add_eq_left_iff 📖	mathematical	—	Cardinal instAdd instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0 instZero	—	max_le_iff le_or_gt not_lt ne_of_gt LT.lt.trans_le self_le_add_left canonicallyOrderedAdd lt_aleph0 add_lt_aleph0_iff Nat.cast_zero instCharZero AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero add_eq_max max_eq_left
add_eq_max 📖	mathematical	Cardinal instLE aleph0	instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	le_antisymm add_le_add addLeftMono addRightMono le_max_left le_max_right add_eq_self LE.le.trans max_le self_le_add_right canonicallyOrderedAdd self_le_add_left
add_eq_max' 📖	mathematical	Cardinal instLE aleph0	instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	add_comm max_comm add_eq_max
add_eq_right 📖	mathematical	Cardinal instLE aleph0	instAdd	—	add_comm add_eq_left
add_eq_right_iff 📖	mathematical	—	Cardinal instAdd instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0 instZero	—	add_comm add_eq_left_iff
add_eq_self 📖	mathematical	Cardinal instLE aleph0	instAdd	—	le_antisymm two_mul mul_eq_self mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd LE.le.trans natCast_le_aleph0 self_le_add_left
add_le_add_iff_of_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	instLE instAdd	—	Mathlib.Tactic.Contrapose.contrapose₁ not_le lt_iff_le_and_ne le_imp_le_of_le_of_le add_le_add_left addRightMono le_refl add_right_inj_of_lt_aleph0
add_le_max 📖	mathematical	—	Cardinal instLE instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	le_or_gt add_eq_max le_max_left add_comm max_comm le_max_of_le_right LT.lt.le add_lt_aleph0
add_le_of_le 📖	mathematical	Cardinal instLE aleph0	instAdd	—	LE.le.trans add_le_add addLeftMono addRightMono le_of_eq add_eq_self
add_lt_add 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	instAdd	—	le_or_gt add_lt_of_lt lt_of_lt_of_le canonicallyOrderedAdd add_lt_aleph0_iff lt_of_le_of_lt add_le_add_iff_of_lt_aleph0 LT.lt.trans LT.lt.le add_comm add_lt_add_iff_of_right_lt_aleph0
add_lt_add_iff_of_left_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	instAdd	—	add_comm add_lt_add_iff_of_right_lt_aleph0
add_lt_add_iff_of_right_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	instAdd	—	Mathlib.Tactic.Contrapose.contrapose₁ add_le_add_iff_of_lt_aleph0
add_lt_of_lt 📖	mathematical	Cardinal instLE aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder	instAdd	—	LE.le.trans_lt add_le_add addLeftMono addRightMono le_max_left le_max_right lt_or_ge LT.lt.trans_le add_lt_aleph0 add_eq_self max_lt
add_mk_eq_max 📖	mathematical	—	Cardinal instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	add_eq_max
add_mk_eq_max' 📖	mathematical	—	Cardinal instAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	add_eq_max'
add_mk_eq_self 📖	mathematical	—	Cardinal instAdd	—	add_mk_eq_max max_self
add_nat_eq 📖	mathematical	Cardinal instLE aleph0	instAdd instNatCast	—	add_eq_left LE.le.trans natCast_le_aleph0
add_nat_inj 📖	mathematical	—	Cardinal instAdd instNatCast	—	add_right_inj_of_lt_aleph0 natCast_lt_aleph0
add_nat_le_add_nat_iff 📖	mathematical	—	Cardinal instLE instAdd instNatCast	—	add_le_add_iff_of_lt_aleph0 natCast_lt_aleph0
add_one_eq 📖	mathematical	Cardinal instLE aleph0	instAdd instOne	—	add_one_of_aleph0_le
add_one_inj 📖	mathematical	—	Cardinal instAdd instOne	—	add_right_inj_of_lt_aleph0 one_lt_aleph0
add_one_le_add_one_iff 📖	mathematical	—	Cardinal instLE instAdd instOne	—	add_le_add_iff_of_lt_aleph0 one_lt_aleph0
add_right_inj_of_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	instAdd	—	eq_of_add_eq_add_right
aleph0_mul_aleph 📖	mathematical	—	Cardinal instMul aleph0 DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph	—	aleph0_mul_eq aleph0_le_aleph
aleph0_mul_eq 📖	mathematical	Cardinal instLE aleph0	instMul	—	mul_eq_max le_rfl max_eq_right
aleph0_mul_mk_eq 📖	mathematical	—	Cardinal instMul aleph0	—	aleph0_mul_eq
aleph_add_aleph 📖	mathematical	—	Cardinal instAdd DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot	—	add_eq_max aleph0_le_aleph aleph_max
aleph_mul_aleph 📖	mathematical	—	Cardinal instMul DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot	—	mul_eq_max aleph0_le_aleph aleph_max
aleph_mul_aleph0 📖	mathematical	—	Cardinal instMul DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph aleph0	—	mul_aleph0_eq aleph0_le_aleph
ciSup_add 📖	mathematical	BddAbove Cardinal instLE Set.range	instAdd iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	le_imp_le_of_le_of_le add_le_add_left addRightMono le_ciSup le_refl le_antisymm Set.forall_mem_range lt_or_ge exists_eq_of_iSup_eq_of_not_isSuccLimit not_isSuccLimit_of_lt_aleph0 add_eq_max max_le_iff ciSup_mono self_le_add_right canonicallyOrderedAdd LE.le.trans self_le_add_left ciSup_le'
ciSup_add_ciSup 📖	mathematical	BddAbove Cardinal instLE Set.range	instAdd iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	ciSup_add add_ciSup
ciSup_mul 📖	mathematical	—	Cardinal instMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	isEmpty_or_nonempty ciSup_of_empty bot_eq_zero' canonicallyOrderedAdd MulZeroClass.zero_mul eq_or_ne MulZeroClass.mul_zero ciSup_const le_imp_le_of_le_of_le le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono le_ciSup le_antisymm Set.forall_mem_range lt_or_ge exists_eq_of_iSup_eq_of_not_isSuccLimit not_isSuccLimit_of_lt_aleph0 mul_eq_max_of_aleph0_le_left max_le_iff exists_lt_of_lt_ciSup' LT.lt.trans_le one_lt_aleph0 ciSup_mono le_mul_right LE.le.trans le_mul_left LT.lt.ne' LT.lt.trans zero_lt_one IsOrderedRing.toZeroLEOneClass isOrderedRing NeZero.charZero_one instCharZero ciSup_le' csSup_of_not_bddAbove csSup_empty
ciSup_mul_ciSup 📖	mathematical	—	Cardinal instMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	ciSup_mul mul_ciSup
eq_of_add_eq_add_left 📖	—	Cardinal instAdd Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	—	—	le_or_gt LT.lt.trans_le eq_of_add_eq_of_aleph0_le add_eq_right LT.lt.le not_le lt_irrefl LE.le.trans_lt LE.le.trans self_le_add_left canonicallyOrderedAdd add_lt_aleph0 lt_aleph0 instCharZero add_left_cancel AddLeftCancelSemigroup.toIsLeftCancelAdd
eq_of_add_eq_add_right 📖	—	Cardinal instAdd Preorder.toLT PartialOrder.toPreorder partialOrder aleph0	—	—	eq_of_add_eq_add_left add_comm
eq_of_add_eq_of_aleph0_le 📖	—	Cardinal instAdd Preorder.toLT PartialOrder.toPreorder partialOrder instLE aleph0	—	—	le_antisymm self_le_add_left canonicallyOrderedAdd not_lt add_lt_of_lt
extend_function 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Set Set.instMembership Function.Embedding Set.Elem Function.instFunLikeEmbedding	—	Function.Embedding.inj' Equiv.Set.sumCompl_symm_apply_of_mem
extend_function_finite 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Set Set.instMembership Function.Embedding Set.Elem Function.instFunLikeEmbedding	—	extend_function lift_mk_eq' mk_compl_eq_mk_compl_finite_lift mk_range_eq_of_injective Function.Embedding.inj'
extend_function_of_lt 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Set Set.instMembership Function.Embedding Function.instFunLikeEmbedding	—	extend_function_finite Finite.of_fintype extend_function lift_mk_eq' mk_compl_of_infinite Infinite.of_injective Equiv.injective lift_lt mk_range_eq_of_injective Function.Embedding.injective
le_mul_left 📖	mathematical	—	Cardinal instLE instMul	—	one_mul mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd one_le_iff_ne_zero
le_mul_right 📖	mathematical	—	Cardinal instLE instMul	—	mul_comm le_mul_left
mk_add_one_eq 📖	mathematical	—	Cardinal instAdd instOne	—	add_one_eq
mk_arrow_eq_zero_iff 📖	mathematical	—	Cardinal instZero	—	—
mk_bounded_set_le 📖	mathematical	—	Cardinal instLE Set Set.Elem instPowCardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	LE.le.trans mk_image_le mk_bounded_set_le_of_infinite Sum.infinite_of_left instInfiniteULift instInfiniteNat max_comm add_eq_max le_refl
mk_bounded_set_le_of_infinite 📖	mathematical	—	Cardinal instLE Set Set.Elem instPowCardinal	—	add_one_eq inductionOn mk_le_of_surjective le_trans mk_preimage_of_injective mk_range_le Set.ext Function.Embedding.inj'
mk_bounded_subset_le 📖	mathematical	—	Cardinal instLE Set Set.instHasSubset Set.Elem instPowCardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	le_trans Set.preimage_eq_preimage' Subtype.range_coe LE.le.trans mk_preimage_of_injective Subtype.val_injective mk_bounded_set_le
mk_compl_eq_mk_compl_finite 📖	mathematical	Set.Elem	Compl.compl Set Set.instCompl	—	mk_compl_eq_mk_compl_finite_lift
mk_compl_eq_mk_compl_finite_lift 📖	mathematical	lift Set.Elem	Compl.compl Set Set.instCompl	—	nonempty_fintype lift_mk_eq' Fintype.ofEquiv_card CanLift.prf Set.instCanLiftFinsetCoeFinite Set.toFinite Subtype.finite Finite.of_fintype mk_coe_finset Finset.card_compl mk_fintype Fintype.card_coe lift_natCast instCharZero
mk_compl_eq_mk_compl_finite_same 📖	mathematical	Set.Elem	Compl.compl Set Set.instCompl	—	mk_compl_eq_mk_compl_finite
mk_compl_eq_mk_compl_infinite 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	Compl.compl Set Set.instCompl	—	mk_compl_of_infinite
mk_compl_finset_of_infinite 📖	mathematical	—	Set.Elem Compl.compl Set Set.instCompl SetLike.coe Finset Finset.instSetLike	—	mk_compl_of_infinite LT.lt.trans_le finset_card_lt_aleph0
mk_compl_of_infinite 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	Compl.compl Set Set.instCompl	—	eq_of_add_eq_of_aleph0_le mk_sum_compl
mk_embedding_eq_arrow_of_le 📖	mathematical	—	Function.Embedding	—	mk_embedding_eq_arrow_of_lift_le lift_le
mk_embedding_eq_arrow_of_lift_le 📖	mathematical	—	Function.Embedding	—	LE.le.antisymm mk_embedding_le_arrow Equiv.cardinal_eq eq mul_eq_self lift_mk_le' Function.Embedding.injective
mk_embedding_eq_zero_iff_lift_lt 📖	mathematical	—	Function.Embedding Cardinal instZero Preorder.toLT PartialOrder.toPreorder partialOrder lift	—	mk_eq_zero_iff not_nonempty_iff lift_mk_le' not_le
mk_embedding_eq_zero_iff_lt 📖	mathematical	—	Function.Embedding Cardinal instZero Preorder.toLT PartialOrder.toPreorder partialOrder	—	mk_embedding_eq_zero_iff_lift_lt lift_lt
mk_embedding_le_arrow 📖	mathematical	—	Cardinal instLE Function.Embedding	—	DFunLike.coe_injective
mk_equiv_comm 📖	mathematical	—	Equiv	—	Equiv.cardinal_eq Equiv.symm_bijective
mk_equiv_eq_arrow_of_eq 📖	mathematical	—	Equiv	—	mk_equiv_eq_arrow_of_lift_eq
mk_equiv_eq_arrow_of_lift_eq 📖	mathematical	lift	Equiv	—	lift_mk_eq' lift_id' mk_perm_eq_self_power power_def
mk_equiv_eq_zero_iff_lift_ne 📖	mathematical	—	Equiv Cardinal instZero	—	mk_eq_zero_iff not_nonempty_iff lift_mk_eq'
mk_equiv_eq_zero_iff_ne 📖	mathematical	—	Equiv Cardinal instZero	—	mk_equiv_eq_zero_iff_lift_ne lift_id
mk_equiv_le_embedding 📖	mathematical	—	Cardinal instLE Equiv Function.Embedding	—	Equiv.toEmbedding_injective
mk_equiv_of_eq 📖	mathematical	—	Equiv Cardinal instPowCardinal instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mk_equiv_of_lift_eq lift_id
mk_equiv_of_lift_eq 📖	mathematical	lift	Equiv Cardinal instPowCardinal instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat lift_mk_eq' lift_id' lift_umax mk_perm_eq_two_power lift_power lift_natCast
mk_finset_of_infinite 📖	mathematical	—	Finset	—	le_antisymm mk_le_of_injective mk_le_of_surjective List.toFinset_surjective
mk_list_eq_aleph0 📖	mathematical	—	aleph0	—	LE.le.antisymm mk_le_aleph0 List.countable instInfiniteListOfNonempty
mk_list_eq_max 📖	mathematical	—	Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	finite_or_infinite mk_list_eq_aleph0 Finite.to_countable max_eq_left mk_le_aleph0 max_eq_right
mk_list_eq_max_mk_aleph0 📖	mathematical	—	Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_list_eq_max max_comm
mk_list_eq_mk 📖	—	—	—	—	le_antisymm le_def mk_list_eq_sum_pow sum_le_sum pow_le natCast_lt_aleph0 sum_const mk_eq_aleph0 instCountableNat instInfiniteNat lift_aleph0 lift_uzero aleph0_mul_eq
mk_list_le_max 📖	mathematical	—	Cardinal instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	finite_or_infinite LE.le.trans mk_le_aleph0 List.countable Finite.to_countable le_max_left le_max_right
mk_mul_aleph0_eq 📖	mathematical	—	Cardinal instMul aleph0	—	mul_aleph0_eq
mk_perm_eq_self_power 📖	mathematical	—	Equiv.Perm Cardinal instPowCardinal	—	LE.le.antisymm LE.le.trans mk_equiv_le_embedding mk_embedding_le_arrow mk_prod Nat.instAtLeastTwoHAddOfNat lift_uzero mk_fintype lift_ofNat mul_two add_mk_eq_max max_self power_def power_self_eq Equiv.cardinal_eq mk_pi prod_const
mk_perm_eq_two_power 📖	mathematical	—	Equiv.Perm Cardinal instPowCardinal instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mk_perm_eq_self_power power_self_eq
mk_surjective_eq_arrow_of_le 📖	mathematical	—	Set.Elem setOf	—	mk_surjective_eq_arrow_of_lift_le lift_le
mk_surjective_eq_arrow_of_lift_le 📖	mathematical	—	Set.Elem setOf	—	LE.le.antisymm mk_set_le mk_sum lift_add lift_lift lift_umax add_eq_left aleph0_le_lift Equiv.right_inv Equiv.apply_symm_apply
mk_surjective_eq_zero_iff 📖	mathematical	—	Set.Elem setOf Cardinal instZero Preorder.toLT PartialOrder.toPreorder partialOrder	—	mk_surjective_eq_zero_iff_lift lift_lt
mk_surjective_eq_zero_iff_lift 📖	mathematical	—	Set.Elem setOf Cardinal instZero Preorder.toLT PartialOrder.toPreorder partialOrder lift	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_and_or_eq lift_mk_le'
mul_aleph0_eq 📖	mathematical	Cardinal instLE aleph0	instMul	—	mul_eq_max le_rfl max_eq_left
mul_ciSup 📖	mathematical	—	Cardinal instMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mul_comm ciSup_mul
mul_eq_left 📖	mathematical	Cardinal instLE aleph0	instMul	—	mul_eq_max_of_aleph0_le_left max_eq_left
mul_eq_left_iff 📖	mathematical	—	Cardinal instMul instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0 instOne instZero	—	max_le_iff le_or_gt LE.le.not_gt aleph0_pos not_lt ne_of_gt LT.lt.trans_le le_mul_left MulZeroClass.mul_zero lt_aleph0 mul_lt_aleph0_iff Nat.cast_one instCharZero le_antisymm mul_one addLeftMono IsOrderedRing.toZeroLEOneClass isOrderedRing one_le_iff_ne_zero mul_eq_max_of_aleph0_le_left max_eq_left MulZeroClass.zero_mul
mul_eq_max 📖	mathematical	Cardinal instLE aleph0	instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	le_antisymm mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd covariant_swap_mul_of_covariant_mul le_max_left le_max_right mul_eq_self LE.le.trans max_le mul_one mul_le_mul_right one_le_aleph0 one_mul mul_le_mul_left
mul_eq_max' 📖	mathematical	Cardinal instLE aleph0 instMul	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	aleph0_le_mul_iff mul_eq_max_of_aleph0_le_left mul_eq_max_of_aleph0_le_right
mul_eq_max_of_aleph0_le_left 📖	mathematical	Cardinal instLE aleph0	instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	le_or_gt mul_eq_max LE.le.antisymm mul_le_max_of_aleph0_le_left LE.le.trans LT.lt.le max_eq_left mul_one mul_le_mul_right CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd one_le_iff_ne_zero
mul_eq_max_of_aleph0_le_right 📖	mathematical	Cardinal instLE aleph0	instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mul_comm max_comm mul_eq_max_of_aleph0_le_left
mul_eq_right 📖	mathematical	Cardinal instLE aleph0	instMul	—	mul_comm mul_eq_left
mul_eq_self 📖	mathematical	Cardinal instLE aleph0	instMul	—	le_antisymm lt_wf inductionOn ord_eq instIsStrictTotalOrderOfIsWellOrder RelEmbedding.isWellOrder instIsWellOrderProdLex isWellOrder_lt Ordinal.wellFoundedLT le_of_forall_lt Ordinal.typein_surj lt_ord lt_of_le_of_lt max_le_iff le_iff_lt_or_eq irrefl IsStrictOrder.toIrrefl IsStrictTotalOrder.toIsStrictOrder Sum.instIsWellOrderLex instIsWellOrderEmptyRelationOfSubsingleton lt_or_ge LT.lt.trans_le mul_lt_aleph0 Order.IsSuccLimit.succ_lt isSuccLimit_ord Ordinal.typein_lt_type LE.le.trans_lt Ordinal.card_le_card mul_one mul_le_mul_right CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd LE.le.trans one_le_aleph0
mul_le_max 📖	mathematical	—	Cardinal instLE instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	eq_or_ne MulZeroClass.zero_mul sup_of_le_right canonicallyOrderedAdd MulZeroClass.mul_zero sup_of_le_left le_or_gt mul_eq_max_of_aleph0_le_left le_max_left mul_comm max_comm le_max_of_le_right LT.lt.le mul_lt_aleph0
mul_le_max_of_aleph0_le_left 📖	mathematical	Cardinal instLE aleph0	instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mul_eq_self LE.le.trans le_max_left mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd covariant_swap_mul_of_covariant_mul le_max_right
mul_le_max_of_aleph0_le_right 📖	mathematical	Cardinal instLE aleph0	instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mul_comm max_comm mul_le_max_of_aleph0_le_left
mul_lt_of_lt 📖	mathematical	Cardinal instLE aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder	instMul	—	LE.le.trans_lt mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd covariant_swap_mul_of_covariant_mul le_max_left le_max_right lt_or_ge LT.lt.trans_le mul_lt_aleph0 mul_eq_self max_lt
mul_mk_eq_max 📖	mathematical	—	Cardinal instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mul_eq_max
mul_natCast_inj 📖	mathematical	—	Cardinal instMul instNatCast	—	StrictMono.injective mul_natCast_strictMono
mul_natCast_le_mul_natCast 📖	mathematical	—	Cardinal instLE instMul instNatCast	—	StrictMono.le_iff_le mul_natCast_strictMono
mul_natCast_lt_mul_natCast 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder instMul instNatCast	—	StrictMono.lt_iff_lt mul_natCast_strictMono
mul_natCast_strictMono 📖	mathematical	—	StrictMono Cardinal PartialOrder.toPreorder partialOrder instMul instNatCast	—	mul_comm natCast_mul_strictMono
natCast_mul_inj 📖	mathematical	—	Cardinal instMul instNatCast	—	StrictMono.injective natCast_mul_strictMono
natCast_mul_le_natCast_mul 📖	mathematical	—	Cardinal instLE instMul instNatCast	—	StrictMono.le_iff_le natCast_mul_strictMono
natCast_mul_lt_natCast_mul 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder instMul instNatCast	—	StrictMono.lt_iff_lt natCast_mul_strictMono
natCast_mul_strictMono 📖	mathematical	—	StrictMono Cardinal PartialOrder.toPreorder partialOrder instMul instNatCast	—	Nat.cast_one one_mul strictMono_id Nat.cast_add add_mul Distrib.rightDistribClass add_lt_add
nat_add_eq 📖	mathematical	Cardinal instLE aleph0	instAdd instNatCast	—	add_comm add_nat_eq
nat_power_eq 📖	mathematical	Cardinal instLE aleph0	instPowCardinal instNatCast instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	power_eq_two_power Nat.instAtLeastTwoHAddOfNat addLeftMono IsOrderedRing.toZeroLEOneClass isOrderedRing instCharZero LE.le.trans natCast_le_aleph0
pow_eq 📖	mathematical	Cardinal instLE aleph0 instOne Preorder.toLT PartialOrder.toPreorder partialOrder	instPowCardinal	—	LE.le.antisymm pow_le self_le_power
pow_le 📖	mathematical	Cardinal instLE aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder	instPowCardinal	—	lt_aleph0 Nat.cast_zero power_zero le_imp_le_of_le_of_le le_of_lt one_lt_aleph0 le_refl Nat.cast_succ power_add power_one mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd mul_eq_self
power_eq_two_power 📖	mathematical	Cardinal instLE aleph0 instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instPowCardinal	—	Nat.instAtLeastTwoHAddOfNat le_antisymm power_le_power_right power_self_eq
power_le_aleph0 📖	mathematical	Cardinal instLE aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder	instPowCardinal	—	CanLift.prf canLiftCardinalNat sup_of_le_right power_nat_le_max
power_nat_eq 📖	mathematical	Cardinal instLE aleph0	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	—	pow_eq Nat.cast_one addLeftMono IsOrderedRing.toZeroLEOneClass isOrderedRing instCharZero natCast_lt_aleph0
power_nat_le 📖	mathematical	Cardinal instLE aleph0	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	—	pow_le natCast_lt_aleph0
power_nat_le_max 📖	mathematical	—	Cardinal instLE instPowCardinal instNatCast SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	le_or_gt le_max_of_le_left power_nat_le le_max_of_le_right LT.lt.le power_lt_aleph0 natCast_lt_aleph0
power_self_eq 📖	mathematical	Cardinal instLE aleph0	instPowCardinal instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	LE.le.antisymm Nat.instAtLeastTwoHAddOfNat LE.le.trans power_le_power_right LT.lt.le cantor power_mul mul_eq_self le_refl natCast_le_aleph0
powerlt_aleph0 📖	mathematical	Cardinal instLE aleph0	powerlt	—	le_antisymm powerlt_le lt_aleph0 power_nat_le power_one le_powerlt one_lt_aleph0
powerlt_aleph0_le 📖	mathematical	—	Cardinal instLE powerlt aleph0 SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	le_or_gt powerlt_aleph0 le_max_left powerlt_le LE.le.trans LT.lt.le power_lt_aleph0 le_max_right
prod_eq_two_power 📖	mathematical	Cardinal instLE instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat lift	prod instPowCardinal	—	Nat.instAtLeastTwoHAddOfNat lift_id' lift_prod lift_two_power le_antisymm LE.le.trans_eq prod_le_prod prod_const lift_lift lift_power power_self_eq lift_umax prod_const' lift_two lift_le
sum_eq_iSup 📖	mathematical	Cardinal instLE iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	sum	—	sum_eq_iSup_of_mk_le_iSup
sum_eq_iSup_lift 📖	mathematical	Cardinal instLE lift iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	sum	—	sum_eq_iSup_of_lift_mk_le_iSup
sum_eq_iSup_of_lift_mk_le_iSup 📖	mathematical	Cardinal instLE lift iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	sum	—	lift_id' sum_eq_lift_iSup_of_lift_mk_le_lift_iSup UnivLE.small univLE_of_max UnivLE.self lift_umax
sum_eq_iSup_of_mk_le_iSup 📖	mathematical	Cardinal instLE iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	sum	—	sum_eq_iSup_of_lift_mk_le_iSup lift_id
sum_eq_lift_iSup_of_lift_mk_le_lift_iSup 📖	mathematical	Cardinal instLE lift iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	sum	—	LE.le.antisymm' lift_iSup_le_sum mul_eq_max aleph0_le_lift LE.le.trans lift_iSup bddAbove_of_small small_range max_eq_right sum_le_lift_mk_mul_iSup_lift
sum_pow_eq_max_aleph0 📖	mathematical	—	sum Cardinal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	nonempty_out mk_out mk_list_eq_sum_pow mk_list_eq_max
sum_pow_le_max_aleph0 📖	mathematical	—	Cardinal instLE sum Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_out mk_list_eq_sum_pow mk_list_le_max

---

← Back to Index