Def LinearMap.mkContinuousOfExistsBound₂

Modification history

2024-02-27 00:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore(Analysis/NormedSpace): split up OperatorNorm.lean (#10990) …

Modified LinearMap.mkContinuousOfExistsBound₂ View on Github →

2023-05-25 03:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore: golf proofs about `IsBoundedBilinearMap` (#4239) …

Added LinearMap.mkContinuousOfExistsBound₂ View on Github →