support_bindOnSupport — Mathlib

English

The support of p.bindOnSupport f is exactly the union, over all a in the support of p, of the support of the conditional PMF f(a, ha).

Русский

Опора выражения p.bindOnSupport f равна объединению опор условных распределений f(a, ha) по всем a ∈ supp(p).

LaTeX

$$$$ \\mathrm{supp}(p.bindOnSupport f) = \\bigcup_{a \\in \\mathrm{supp}(p)} \\mathrm{supp}(f(a,h)) $$$$

Lean4

@[simp]
theorem support_bindOnSupport : (p.bindOnSupport f).support = ⋃ (a : α) (h : a ∈ p.support), (f a h).support :=
  by
  refine Set.ext fun b => ?_
  simp only [ENNReal.tsum_eq_zero, not_or, mem_support_iff, bindOnSupport_apply, Ne, not_forall, mul_eq_zero,
    Set.mem_iUnion]
  exact
    ⟨fun hb =>
      let ⟨a, ⟨ha, ha'⟩⟩ := hb
      ⟨a, ha, by simpa [ha] using ha'⟩,
      fun hb =>
      let ⟨a, ha, ha'⟩ := hb
      ⟨a, ⟨ha, by simpa [(mem_support_iff _ a).1 ha] using ha'⟩⟩⟩

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