examples showing (C[a, b], sup norm) is a banch space?

Stream: Is there code for X?

[Sayantan Majumdar]

I have been trying to work and have some proof done in functional analysis but I am having some troubles. Has anybody proved that (C[a, b], sup norm) is a Banach space and that C[a, b] with the Euclidean norm is not a Banach space?

I would like to compare my proof with them to see where it goes wrong.

If you guys found any work where proofs using functional analysis, Banach space, compact operators in Banach space etc have been done, please do let me know

[Moritz Doll]

docs#BoundedContinuousFunction.instCompleteSpaceBoundedContinuousFunctionToUniformSpaceInstPseudoMetricSpaceBoundedContinuousFunction and docs#BoundedContinuousFunction.normedSpace for the Banach space

[Moritz Doll]

I don't think we have counterexample to the non-completeness. Learning from mathematics from Lean code is probably not very efficient, I would suggest to figure these thing out on paper.

[Yaël Dillies]

New rule: If someone links a newcomer to an overly long autogenerated instance name without immediately apologising, I open a PR to rename said instance.

[Yaël Dillies]

#10780 is the PR for this tile