instNeZeroMeasureCoeSectROfProdMk

Mathlib.Probability.Kernel.Composition.MapComap

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk

English

If κ(a,b) ≠ 0, then (sectR a) b ≠ 0, i.e. the section at (a,b) is nonzero implies the corresponding left section at a fixes b nonzero.

Русский

Если κ(a,b) ≠ 0, тогда (sectR a) b ≠ 0; секция секции при (a,b) ненулевая.

LaTeX

$$κ(a,b) ≠ 0 ⇒ (sectR a) b ≠ 0$$

Lean4

instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectR κ a) b) := by rw [sectR_apply];
  infer_instance

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

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

Разделы

Аффилиация

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