Commit 2024-03-11 22:04 349b8431

View on Github →

feat(Normed/Group): add lt version of IsBounded.exists_pos_norm_le (#10861)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem Bornology.IsBounded.exists_pos_norm_lt'

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean