This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lncnbd

Description: A continuous linear operator is a bounded linear operator. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	lncnbd	$⊢ LinOp \cap ContOp = BndLinOp$

Step	Hyp	Ref	Expression
1		lncnopbd	$⊢ t \in (LinOp \cap ContOp) \leftrightarrow t \in BndLinOp$
2	1	eqriv	$⊢ LinOp \cap ContOp = BndLinOp$