English
Given a finite set A and a normal subgroup H, an inequality holds relating the cardinalities of certain constructions with quotients and products, extending the previous lemma.
Русский
Пусть A — конечное множество, H — нормальная подгруппа; выполняется неравенство кардиналов, расширяющее предыдущее лемму.
LaTeX
$$$|A| \le |A / H| \cdot |\{x \in A^2 : x \in H\}| \text{ in appropriate contexts}$$$
Lean4
@[to_additive]
theorem le_card_quotient_mul_sq_inter_subgroup (hAsymm : A⁻¹ = A) :
#A ≤ #(A.image <| QuotientGroup.mk' H) * #({x ∈ A ^ 2 | x ∈ H}) := by
classical
set π := QuotientGroup.mk' H
rw [card_eq_sum_card_image π]
refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_
calc
#({a' ∈ A | π a' = π a})
_ ≤ #(({a' ∈ A | π a' = π a})⁻¹ * {a' ∈ A | π a' = π a}) := (card_le_card_mul_left ⟨a⁻¹, by simpa⟩)
_ ≤ #({x ∈ A⁻¹ * A | x ∈ H}) := by
gcongr
simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
rintro x hx hxa y hy hya
refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
simp [hya, ← hxa]
_ = #({x ∈ A ^ 2 | x ∈ H}) := by simp [hAsymm, sq]
