Theorem Seminorm.exists_le_comp_of_isInducing

Modification history

2026-06-11 01:51
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat: Analytic Hahn Banach theorem for locally convex spaces (#38739) …
Added Seminorm.exists_le_comp_of_isInducingView on Github →