isHenstock_single_iff

Mathlib.Analysis.BoxIntegral.Partition.Tagged

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

← MathLib Explorer

English

The single prepartition is Henstock equivalent to x lying in Icc(J).

Русский

Единичное разбиение Хенстокпа эквивалентно условию x ∈ Icc(J).

LaTeX

$$$ IsHenstock\,(single\ I\ J\ hJ\ x\ h) \iff x \in Box.Icc J $$$

Lean4

@[simp]
theorem isHenstock_single_iff (hJ : J ≤ I) (h : x ∈ Box.Icc I) : IsHenstock (single I J hJ x h) ↔ x ∈ Box.Icc J :=
  forall_mem_single (fun x J => x ∈ Box.Icc J) hJ h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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