tacticUniqueDiffWithinAt_Ici_Iic_univ

English

Under standard hypotheses, the derivative of the interval-integral map with respect to (u,v) is the linear functional (h,k) ↦ k cb − h ca.

Русский

Под обычными предпосылками производная от функции ∫_u^v f равна линейному функционалу (h,k) ↦ k cb − h ca.

LaTeX

$$$D(h,k) = k c_b - h c_a.$$$

Lean4

/-- An auxiliary tactic closing goals `UniqueDiffWithinAt ℝ s a` where
`s ∈ {Iic a, Ici a, univ}`. -/
@[tactic_parser 1000]
public meta def tacticUniqueDiffWithinAt_Ici_Iic_univ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `intervalIntegral.tacticUniqueDiffWithinAt_Ici_Iic_univ 1024
    (ParserDescr.nonReservedSymbol✝ "uniqueDiffWithinAt_Ici_Iic_univ" false✝)

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