support_ofFinset — Mathlib

English

The support of the PMF constructed from a Finset s is exactly the intersection of s (viewed as a set) with the finite support of f.

Русский

Опора PMF, полученного из множества Finset s, совпадает с пересечением множества s и множества поддержки f.

LaTeX

$$$ (ofFinset f s h h').support = (↑s) \cap (Function.support f) $$$

Lean4

@[simp]
theorem support_ofFinset : (ofFinset f s h h').support = ↑s ∩ Function.support f :=
  Set.ext fun a => by simpa [mem_support_iff] using mt (h' a)

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