cast_subConst — Mathlib

English

For finite A,B in G', the constant δ[A,B] cast in 𝕜 equals the ratio |A−B|/|A|, where A−B is the set-theoretic difference A \ B.

Русский

Для конечных A,B в G' константа δ[A,B], приведенная в 𝕜, равна отношению |A−B| к |A|, где A−B = A \ B.

LaTeX

$$$\\delta[A,B] = \\dfrac{|A \\setminus B|}{|A|}$$$

Lean4

theorem cast_subConst (A B : Finset G') : (δ[A, B] : 𝕜) = #(A - B) / #A := by simp [subConst]

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