English
Let X be a type with a zero, R a type with a zero and topological spaces on X and R. If f: X → R is continuous and f(0) = 0, then mkD f g is exactly the pair consisting of the function f together with its continuity data and the condition f(0) = 0. In particular mkD f g equals the canonical data built from f and hf.
Русский
Пусть X — множество с нулём, R — множество с нулём; пусть заданы топологические структуры на X и R. Если f: X → R непрерывна и f(0) = 0, то mkD f g равняется паре, содержащей функцию f вместе с её данными о непрерывности и условием f(0) = 0. В частности mkD f g совпадает с каноническими данными, построенными из f и hf.
LaTeX
$$$mkD(f,g) = \\langle \\langle f, hf \\rangle, hf_0 \\rangle$$$
Lean4
theorem mkD_of_continuous [Zero X] {f : X → R} {g : C(X, R)₀} (hf : Continuous f) (hf₀ : f 0 = 0) :
mkD f g = ⟨⟨f, hf⟩, hf₀⟩ := by simp only [mkD, And.intro hf hf₀, true_and, ↓reduceDIte]
