rCond_of_bRiemann_eq_false

Mathlib.Analysis.BoxIntegral.Partition.Filter

URI: https://scilib.ai/kg/mathlib#BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false

← MathLib Explorer

English

If l.bRiemann = false, then l.RCond r holds for any r.

Русский

Если l.bRiemann = false, то l.RCond r выполняется для любого r.

LaTeX

$$$l.bRiemann = \\text{false} \\Rightarrow l.RCond r$$$

Lean4

theorem rCond_of_bRiemann_eq_false {ι} (l : IntegrationParams) (hl : l.bRiemann = false) {r : (ι → ℝ) → Ioi (0 : ℝ)} :
    l.RCond r := by simp [RCond, hl]

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

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

Разделы

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

Аффилиация

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