indepSet_empty_left — Mathlib

English

Independence holds when testing against the empty right-hand set: the empty set contributes neutral element.

Русский

Независимость по отношению к пустому множеству справа: пустое множество вносит нейтральный элемент.

LaTeX

$$$ IndepSet s ∅ κ μ$$$

Lean4

theorem indepSet_empty_left {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ]
    (s : Set Ω) : IndepSet ∅ s κ μ :=
  (indepSet_empty_right s).symm

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