instIsZeroOrMarkovKernelSectROfProd

English

If κ is zero-or-Markov, then for any a ∈ α, sectR κ a is zero-or-Markov.

Русский

Если κ имеет свойство нуль-или-маркоровское, то для любого a секция sectR κ a сохраняет это свойство.

LaTeX

$$IsZeroOrMarkovKernel κ ⇒ IsZeroOrMarkovKernel (sectR κ a)$$

Lean4

instance (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (sectR κ a) := by rw [sectR];
  infer_instance

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