isHenstock_single

Mathlib.Analysis.BoxIntegral.Partition.Tagged

URI: https://scilib.ai/kg/mathlib#BoxIntegral.TaggedPrepartition.isHenstock_single

English

If x ∈ Box.Icc I, then the singleton prepartition with J = I is Henstock.

Русский

Если x ∈ Box.Icc I, то единичное разбиение с J = I — Хенштокг.

LaTeX

$$$ IsHenstock (single I I le\_rfl x h) $$$

Lean4

theorem isHenstock_single (h : x ∈ Box.Icc I) : IsHenstock (single I I le_rfl x h) :=
  (isHenstock_single_iff (le_refl I) h).2 h

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

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

Разделы

Аффилиация

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