mem_support_uniformOfFintype

Mathlib.Probability.Distributions.Uniform

URI: https://scilib.ai/kg/mathlib#PMF.mem_support_uniformOfFintype

English

An element belongs to the support of uniformOfFintype α if and only if it is in α.

Русский

Элемент принадлежит опоре uniformOfFintype α тогда и только тогда, когда он находится в α.

LaTeX

$$$a\\in (uniformOfFintype\\;\\alpha).\\text{support} \\iff a\\in \\alpha$$$

Lean4

theorem mem_support_uniformOfFintype (a : α) : a ∈ (uniformOfFintype α).support := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru