lineDerivWithin_congr' — Mathlib

English

If s and t are event-equal in a neighborhood of x via a standard parametrization, then HasLineDerivWithinAt for s is equivalent to HasLineDerivWithinAt for t.

Русский

Если множества s и t эквивалентны в окрестности x через стандартную параметризацию, то HasLineDerivWithinAt для s эквивалентно HasLineDerivWithinAt для t.

LaTeX

$$$\bigl(s =^\mathcal{N} x t\bigr) \Rightarrow (\text{HasLineDerivWithinAt}_{\mathbb{k}}(f,f',s,x,v) \iff \text{HasLineDerivWithinAt}_{\mathbb{k}}(f,f',t,x,v))$$$

Lean4

theorem lineDerivWithin_congr' (hs : EqOn f₁ f s) (hx : x ∈ s) :
    lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v :=
  lineDerivWithin_congr hs (hs hx)

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