condKernelCountable_apply — Mathlib

English

For any h_atom, and p = (a,b), condKernelCountable κCond h_atom p = κCond a b.

Русский

Для любого h_atom и p = (a,b) выполняется condKernelCountable κCond h_atom p = κCond a b.

LaTeX

$$$\\text{condKernelCountable}(κCond,h_{atom})\\;p = κCond(p.fst,p.snd).$$$

Lean4

theorem condKernelCountable_apply (h_atom : ∀ x y, x ∈ measurableAtom y → κCond x = κCond y) (p : α × β) :
    condKernelCountable κCond h_atom p = κCond p.1 p.2 :=
  rfl

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