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

condRho_of_injective

PFR.RhoFunctional · PFR/RhoFunctional.lean:889 to 904

Source documentation

If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$ .

Exact Lean statement

lemma condRho_of_injective {S T : Type*}
    (Y : Ω → S) {A : Finset G} {f : S → T} (hf : Function.Injective f) :
    ρ[X | f ∘ Y ; μ # A] = ρ[X | Y ; μ # A]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRho_of_injective {S T : Type*}    (Y : Ω → S) {A : Finset G} {f : S → T} (hf : Function.Injective f) :    ρ[X | f ∘ Y ; μ # A] = ρ[X | Y ; μ # A] := by  simp only [condRho]  rw [← hf.tsum_eq]  · have I c : f ∘ Y ⁻¹' {f c} = Y ⁻¹' {c} := by      ext z; simp [hf.eq_iff]    simp [I]  · intro y hy    have : f ∘ Y ⁻¹' {y} ≠ ∅ := by      intro h      simp [h] at hy    rcases Set.nonempty_iff_ne_empty.2 this with ⟨a, ha⟩    simp only [mem_preimage, Function.comp_apply, mem_singleton_iff] at ha    rw [← ha]    exact mem_range_self (Y a)