Structure IsBoundedLinearMap

Modification history

2024-09-23 11:56

Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

chore: generalize `IsBoundedBilinearMap` to seminormed spaces (#17011) …

Modified IsBoundedLinearMap View on Github →

2023-08-10 19:52

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified IsBoundedLinearMap View on Github →

2023-05-20 10:55

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

feat: port Analysis.NormedSpace.BoundedLinearMaps (#4091) …

Added IsBoundedLinearMap View on Github →