card_inv_mul_of_doubling_lt_three_halves

English

For doubling less than 3/2, the cardinalities satisfy a stable equality: #(A⁻¹ A) = #(A A).

Русский

При удвоении менее чем 3/2 выполняется равенство кардиналий: #(A⁻¹ A) = #(A A).

LaTeX

$$$#(A^{-1} A) = #(A A)$$$

Lean4

theorem card_inv_mul_of_doubling_lt_three_halves (h : #(A * A) < (3 / 2 : ℚ) * #A) : #(A⁻¹ * A) = #(A * A) :=
  by
  obtain ⟨a, ha⟩ := nonempty_of_doubling h
  simp_rw [← smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves h ha, card_smul_finset]

Похожие утверждения