Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.setRuzsaDist_symm

PFR.ForMathlib.Entropy.RuzsaSetDist · PFR/ForMathlib/Entropy/RuzsaSetDist.lean:44 to 52

Source documentation

Ruzsa distance between sets is symmetric.

Exact Lean statement

lemma setRuzsaDist_symm (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B] :
    dᵤ[A # B] = dᵤ[B # A]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma setRuzsaDist_symm (A B : Set G) [hA : Finite A] [hB : Finite B] [Nonempty A] [Nonempty B] :    dᵤ[A # B] = dᵤ[B # A] := by  obtain ⟨Ω, mΩ, UA, hμ, hUA_mes, hUA_unif, -, -⟩ :=    exists_isUniform_measureSpace' A hA .of_subtype  obtain ⟨Ω', mΩ', UB, hμ', hUB_mes, hUB_unif, -, -⟩ :=    exists_isUniform_measureSpace' B hB .of_subtype  rw [setRuzsaDist_eq_rdist hUA_unif hUB_unif hUA_mes hUB_mes,    setRuzsaDist_eq_rdist hUB_unif hUA_unif hUB_mes hUA_mes]  exact rdist_symm