The Lean 4 theorem `isUniformInducing_toComplL` in the `ChapterFriedrichsExtension` chapter of the timepiece formalization

Proved

BookProof.FriedrichsExtension.FormDom.isUniformInducing_toComplL

by leonardopedro · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem isUniformInducing_toComplL in the ChapterFriedrichsExtension chapter of the timepiece formalization.

Preamble

-- Generated from ChapterFriedrichsExtension.lean — theorem BookProof.FriedrichsExtension.FormDom.isUniformInducing_toComplL
import Mathlib
import Definitions.Def_ChapterFriedrichsExtension
open BookProof.FriedrichsExtension
open BookProof.FriedrichsExtension.FormDom



open BookProof.FarisLavine BookProof.YangMillsFriedrichs BookProof.HashimotoShiftInvert
open BookProof.HermiteGalerkin

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]

Formal statement

theorem BookProof.FriedrichsExtension.FormDom.isUniformInducing_toComplL (P : PosSymOp F) :
    IsUniformInducing (UniformSpace.Completion.toComplL (𝕜 := ℂ) (E := FormDom P)) := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterFriedrichsExtension.lean

View graph