differentiableOn_univ — Mathlib

English

If h : DifferentiableOn 𝕜 f t and s ⊆ t then DifferentiableOn 𝕜 f s.

Русский

Если h : DifferentiableOn 𝕜 f t, и s ⊆ t, тогда DifferentiableOn 𝕜 f s.

LaTeX

$$$\text{DifferentiableOn } 𝕜 f t \Rightarrow (s \subset t) \Rightarrow \text{DifferentiableOn } 𝕜 f s$$$

Lean4

theorem differentiableOn_univ : DifferentiableOn 𝕜 f univ ↔ Differentiable 𝕜 f := by
  simp only [DifferentiableOn, Differentiable, differentiableWithinAt_univ, mem_univ, forall_true_left]

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