Module docstring
{"# Cardinalities of pointwise operations on sets "}
Cardinal.mk_mul_le
theorem
: #(s * t) ≤ #s * #t
Full source
@[to_additive]
lemma _root_.Cardinal.mk_mul_le : #(s * t) ≤ #s * #t := by
rw [← image2_mul]; exact Cardinal.mk_image2_leInformal description
For any two sets $s$ and $t$, the cardinality of their pointwise product $s \cdot t$ is less than or equal to the product of their cardinalities, i.e.,
$$\#(s \cdot t) \leq \#s \cdot \#t.$$
Set.natCard_mul_le
theorem
: Nat.card (s * t) ≤ Nat.card s * Nat.card t
Full source
@[to_additive]
lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
obtain h | h := (s * t).infinite_or_finite
· simp [Set.Infinite.card_eq_zero h]
simp only [Nat.card, ← Cardinal.toNat_mul]
refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_
aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])Informal description
For any two sets $s$ and $t$ in a multiplicative structure, the natural number cardinality of their pointwise product $s \cdot t$ is less than or equal to the product of their natural number cardinalities, i.e.,
$$\mathrm{Nat.card}(s \cdot t) \leq \mathrm{Nat.card}(s) \cdot \mathrm{Nat.card}(t).$$
Cardinal.mk_inv
theorem
(s : Set G) : #↥(s⁻¹) = #s
Full source
@[to_additive (attr := simp)]
lemma _root_.Cardinal.mk_inv (s : Set G) : #↥(s⁻¹) = #s := by
rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]Informal description
For any subset $s$ of a group $G$, the cardinality of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the cardinality of $s$, i.e., $\#(s^{-1}) = \#s$.
Set.natCard_inv
theorem
(s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s
Full source
@[to_additive (attr := simp)]
lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by
rw [← image_inv_eq_inv, Nat.card_image_of_injective inv_injective]Informal description
For any subset $s$ of a group $G$, the natural number cardinality of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the natural number cardinality of $s$, i.e., $\mathrm{Nat.card}(s^{-1}) = \mathrm{Nat.card}(s)$.
Set.encard_inv
theorem
(s : Set G) : s⁻¹.encard = s.encard
Full source
@[to_additive (attr := simp)]
lemma encard_inv (s : Set G) : s⁻¹.encard = s.encard := by
simp [ENat.card, ← toENat_cardinalMk]Informal description
For any subset $s$ of a group $G$, the extended cardinality of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the extended cardinality of $s$, i.e., $\mathrm{encard}(s^{-1}) = \mathrm{encard}(s)$.
Set.ncard_inv
theorem
(s : Set G) : s⁻¹.ncard = s.ncard
Informal description
For any subset $s$ of a group $G$, the natural cardinality of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the natural cardinality of $s$, i.e., $|s^{-1}| = |s|$.
Cardinal.mk_div_le
theorem
: #(s / t) ≤ #s * #t
Full source
@[to_additive]
lemma _root_.Cardinal.mk_div_le : #(s / t) ≤ #s * #t := by
rw [← image2_div]; exact Cardinal.mk_image2_leInformal description
For any sets $s$ and $t$ in a group $G$, the cardinality of the pointwise division set $s / t := \{a / b \mid a \in s, b \in t\}$ is bounded by the product of the cardinalities of $s$ and $t$, i.e.,
$$\#(s / t) \leq \#s \cdot \#t.$$
Set.natCard_div_le
theorem
: Nat.card (s / t) ≤ Nat.card s * Nat.card t
Full source
@[to_additive]
lemma natCard_div_le : Nat.card (s / t) ≤ Nat.card s * Nat.card t := by
rw [div_eq_mul_inv, ← natCard_inv t]; exact natCard_mul_leInformal description
For any subsets $s$ and $t$ of a group $G$, the natural number cardinality of the pointwise division set $s / t := \{a / b \mid a \in s, b \in t\}$ satisfies the inequality
$$\mathrm{Nat.card}(s / t) \leq \mathrm{Nat.card}(s) \cdot \mathrm{Nat.card}(t).$$
Cardinal.mk_smul_set
theorem
(a : G) (s : Set α) : #↥(a • s) = #s
Full source
@[to_additive (attr := simp)]
lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s :=
Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective a).injOnInformal description
For any element $a$ of a group $G$ acting on a type $\alpha$, and any subset $s \subseteq \alpha$, the cardinality of the dilated set $a \cdot s$ equals the cardinality of $s$, i.e., $\#(a \cdot s) = \#s$.
Set.natCard_smul_set
theorem
(a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s
Full source
@[to_additive (attr := simp)]
lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s :=
Nat.card_image_of_injective (MulAction.injective a) _Informal description
For any element $a$ of a group $G$ acting on a type $\alpha$, and any subset $s \subseteq \alpha$, the cardinality (as a natural number) of the dilated set $a \cdot s$ equals the cardinality of $s$, i.e., $\mathrm{card}(a \cdot s) = \mathrm{card}(s)$. If $s$ is infinite, both cardinalities are zero.
Set.encard_smul_set
theorem
(a : G) (s : Set α) : (a • s).encard = s.encard
Full source
@[to_additive (attr := simp)]
lemma encard_smul_set (a : G) (s : Set α) : (a • s).encard = s.encard := by
simp [ENat.card, ← toENat_cardinalMk]Informal description
For any element $a$ of a group $G$ acting on a type $\alpha$, and any subset $s \subseteq \alpha$, the extended cardinality of the dilated set $a \cdot s$ equals the extended cardinality of $s$, i.e., $\mathrm{encard}(a \cdot s) = \mathrm{encard}(s)$.
Set.ncard_smul_set
theorem
(a : G) (s : Set α) : (a • s).ncard = s.ncard
Full source
@[to_additive (attr := simp)]
lemma ncard_smul_set (a : G) (s : Set α) : (a • s).ncard = s.ncard := by simp [ncard]Informal description
For any element $a$ of a group $G$ acting on a type $\alpha$, and any subset $s \subseteq \alpha$, the natural cardinality of the dilated set $a \cdot s$ equals the natural cardinality of $s$, i.e., $\mathrm{ncard}(a \cdot s) = \mathrm{ncard}(s)$.