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 ∩ ContOp ) = BndLinOp

Proof

Step Hyp Ref Expression
1 lncnopbd ⊢ ( 𝑡 ∈ ( LinOp ∩ ContOp ) ↔ 𝑡 ∈ BndLinOp )
2 1 eqriv ⊢ ( LinOp ∩ ContOp ) = BndLinOp