support_seq — Mathlib

English

The support of the sequence pmf equals the union over all f in the support of q of the image of p.support under f.

Русский

Опора последовательности PMF равна объединению по всем f из опоры q образа множества опоры p через f.

LaTeX

$$$ (seq q p).support = \bigcup_{f \in q.support} f'' p.support $$$

Lean4

@[simp]
theorem support_seq : (seq q p).support = ⋃ f ∈ q.support, f '' p.support :=
  Set.ext fun b => by simp [-mem_support_iff, seq, @eq_comm β b]

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