RCond

Mathlib.Analysis.BoxIntegral.Partition.Filter

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

← MathLib Explorer

English

Equivalence form of RCond under certain parameterization.

Русский

Эквивалентная форма RCond при некоторых параметрах.

LaTeX

$$$(l,r) \\Rightarrow l.RCond r$ with appropriate equivalences$$

Lean4

/-- A predicate saying that in case `l.bRiemann = true`, the function `r` is a constant. -/
def RCond {ι : Type*} (l : IntegrationParams) (r : (ι → ℝ) → Ioi (0 : ℝ)) : Prop :=
  l.bRiemann → ∀ x, r x = r 0

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

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

Разделы

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

Аффилиация

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