Theorems · Theorem · functional analysis
FiniteDimensional.complete
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : UniformSpace E] [T2Space E] [IsUniformAddGroup E] [inst_6 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E], CompleteSpace E
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- AddCommGroupstatement and proof · cited by 12,871
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Equiv.symmproof · cited by 3,681
- CompleteSpacestatement and proof · cited by 2,532
- UniformSpacestatement and proof · cited by 2,040
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankproof · cited by 1,770
- T2Spacestatement and proof · cited by 1,351
- ContinuousSMulstatement and proof · cited by 1,016
Cited by29
Results whose statement or proof uses this declaration.
- LinearMap.adjoint_inner_leftproof · cited by 8
- LinearMap.adjoint_inner_rightproof · cited by 6
- LinearMap.ker_adjoint_comp_selfproof · cited by 4
- LinearMap.adjoint_eq_toCLM_adjointstatement · cited by 2
- LinearMap.orthogonal_kerproof · cited by 2
- LinearMap.IsPositive.conj_adjointproof · cited by 2
- LinearMap.isStarProjection_toContinuousLinearMap_iffstatement · cited by 1
- HasStrictFDerivAt.implicitToOpenPartialHomeomorph_selfproof · cited by 1
- LinearMap.normDet_sqproof · cited by 1
- ContinuousLinearMap.adjoint_toLinearMapstatement · cited by 1
- HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_sourceproof · cited by 1
- Submodule.complete_of_finiteDimensionalproof · cited by 1