mkD_of_continuousOn — Mathlib

English

If f is continuous on s, then mkD(s.restrict f) g equals ⟨s.restrict f, hf.restrict⟩.

Русский

Если f непрерывна на s, тогда mkD (s.restrict f) g = ⟨s.restrict f, hf.restrict⟩.

LaTeX

$$$mkD(s.restrict f)\, g = \langle s.restrict f, hf.restrict \rangle$$$

Lean4

theorem mkD_of_continuousOn {s : Set α} {f : α → β} {g : C(s, β)} (hf : ContinuousOn f s) :
    mkD (s.restrict f) g = ⟨s.restrict f, hf.restrict⟩ :=
  mkD_of_continuous hf.restrict

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