Documentation Verification Report

Dual

📁 Source: Mathlib/Analysis/Normed/Module/Dual.lean

Statistics

Metric	Count
Definitions `Dual`, `inclusionInDoubleDual`, `inclusionInDoubleDualLi`	3
Theorems `polar_AbsConvex`, `closedBall_inv_subset_polar_closedBall`, `double_dual_bound`, `dual_def`, `eq_iff_forall_dual_eq`, `eq_zero_iff_forall_dual_eq_zero`, `eq_zero_of_forall_dual_eq_zero`, `inclusionInDoubleDual_norm_eq`, `inclusionInDoubleDual_norm_le`, `isBounded_polar_of_mem_nhds_zero`, `isClosed_polar`, `norm_le_dual_bound`, `polar_ball`, `polar_ball_subset_closedBall_div`, `polar_closedBall`, `polar_closure`, `sInter_polar_eq_closedBall`, `smul_mem_polar`	18
Total	21

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`polar_AbsConvex` 📖	mathematical	—	`AbsConvex` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `RCLike.toPartialOrder` `polar`	—	`Algebra.to_smulCommClass` `polar_eq_biInter_preimage` `AbsConvex.iInter₂` `Balanced.mulActionHom_preimage` `balanced_closedBall_zero` `SemilinearMapClass.toMulActionSemiHomClass` `semilinearMapClass` `Convex.linear_preimage` `convex_RCLike_iff_convex_real` `IsScalarTower.right` `convex_closedBall`

Module

Definitions

Name	Category	Theorems
`Dual` 📖	CompOp	361 math math: `LieAlgebra.IsKilling.rootSystem_toLinearMap_apply`, `CliffordAlgebra.contractRight_algebraMap_mul`, `instNontrivialDual`, `LinearMap.apply_symm_toPerfPair_self`, `CliffordAlgebra.contractRight_algebraMap`, `RootPairing.posRootForm_posForm_apply_apply`, `LinearMap.BilinForm.dualSubmoduleToDual_apply_apply`, `CliffordAlgebra.contractRight_eq`, `RootPairing.linearIndepOn_root_baseOf'`, `LinearMap.BilinForm.dualSubmoduleToDual_injective`, `Subspace.dualAnnihilator_dualAnnihilator_eq_map`, `RootPairing.Polarization_apply`, `LinearEquiv.flip_apply`, `RootPairing.root'In_corootSpanMem_eq_pairingIn`, `dotProductEquiv_symm_apply`, `PiTensorProduct.dualDistribEquivOfBasis_symm_apply`, `Subspace.instModuleDualFiniteDimensional`, `Submodule.map_dualCoannihilator_le`, `LinearEquiv.coe_toLinearMap_flip`, `CommRing.Pic.mk_dual`, `Basis.toDual_linearCombination_left`, `Basis.dualBasis_coord_toDualEquiv_apply`, `forall_dual_apply_eq_zero_iff`, `Subspace.dualLift_of_subtype`, `Subspace.dualRestrict_comp_dualLift`, `RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm`, `Submodule.dualQuotEquivDualAnnihilator_apply`, `LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `exists_dual_forall_apply_eq_one`, `LieAlgebra.IsKilling.rootSystem_coroot_apply`, `Submodule.quotDualCoannihilatorToDual_apply`, `Dual.eval_comp_comp_evalEquiv_eq`, `Submodule.dualPairing_apply`, `dualMap_dualMap_eq_iff`, `Basis.dual_rank_eq`, `LieAlgebra.lieCharacterEquivLinearDual_apply`, `CliffordAlgebra.contractRight_mul_ι`, `contractLeft_assoc_coevaluation`, `Basis.flag_le_ker_dual`, `LinearEquiv.dualMap_trans`, `Basis.coe_dualBasis`, `RootPairing.coroot'In_rootSpanMem_eq_pairingIn`, `Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff`, `Subspace.dualAnnihilator_dualAnnihilator_eq`, `LieModule.exists_nontrivial_weightSpace_of_lieIdeal`, `zero_prodMap_dualTensorHom`, `RootPairing.span_coroot'_eq_top`, `eval_apply_injective`, `Submodule.dualAnnihilator_map_dualMap_le`, `Submodule.dualCopairing_eq`, `Submodule.quotDualCoannihilatorToDual_nondegenerate`, `RootPairing.Hom.weight_coweight_transpose`, `DualBases.coe_dualBasis`, `Submodule.mem_dualAnnihilator`, `RootPairing.toPerfPair_comp_root`, `Submodule.dualAnnihilator_eq_top_iff`, `TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse`, `CliffordAlgebra.contractRight_comm`, `TensorProduct.dualDistrib_apply_comm`, `Submodule.coe_dualCoannihilator_span`, `Basis.toDualEquiv_apply`, `RootPairing.root'_coroot_eq_pairing`, `dotProductEquiv_apply_apply`, `RootPairing.injOn_dualMap_subtype_span_root_coroot`, `LinearMap.trace_eq_contract_of_basis'`, `Basis.linearEquiv_dual_iff_finiteDimensional`, `mapEvalEquiv_apply`, `Subspace.finrank_dualCoannihilator_eq`, `exteriorPower.ιMultiDual_apply_diag`, `DualBases.eval_of_ne`, `Subspace.finiteDimensional_quot_dualCoannihilator_iff`, `LinearMap.toMatrix_transpose`, `LinearMap.extendTo𝕜'_apply`, `LinearMap.isSymm_dualProd`, `LinearMap.dualMap_surjective_of_injective`, `subsingleton_dual_iff`, `Submodule.dualAnnihilator_anti`, `dual_finite`, `LinearMap.trace_eq_contract`, `CliffordAlgebra.changeFormAux_apply_apply`, `Subspace.dualPairing_nondegenerate`, `SeparatingDual.dualMap_surjective_iff`, `dualTensorHom_apply`, `Submodule.dualCoannihilator_iSup_eq`, `comap_eval_surjective`, `LinearMap.dualMap_id`, `CliffordAlgebra.changeForm_ι_mul`, `RootPairing.corootSpan_map_flip_toPerfPair`, `coevaluation_apply_one`, `Submodule.dualRestrict_ker_eq_dualAnnihilator`, `IsBaseChange.transvection`, `LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top`, `Dual.eval_apply`, `LinearMap.trace_eq_contract_apply`, `dualTensorHomEquivOfBasis_symm_cancel_right`, `LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'`, `CommRing.Pic.inv_eq_dual`, `LinearMap.IsPerfectCompl.isCompl_right`, `LinearMap.trace_transpose'`, `Dual.transpose_apply`, `Invertible.instDual`, `Submodule.comap_dualAnnihilator`, `LinearMap.dualProd_apply_apply`, `TensorProduct.dualDistribEquivOfBasis_symm_apply`, `dual_free`, `Matrix.toPerfectPairing_apply_apply`, `Submodule.iSup_dualAnnihilator_le_iInf`, `LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `QuadraticForm.dualProd_apply`, `Basis.toDual_ker`, `Basis.dualBasis_apply_self`, `LieAlgebra.lieCharacterEquivLinearDual_symm_apply`, `LinearMap.trace_eq_contract'`, `LinearEquiv.symm_flip`, `LinearMap.extendTo𝕜_apply`, `LinearMap.range_dualMap_eq_dualAnnihilator_ker`, `Submodule.dualCoannihilator_map_linearEquiv_flip`, `RootPairing.rootSpan_map_toPerfPair`, `RootPairing.coroot'_apply_apply_mem_of_mem_span`, `Basis.dualBasis_equivFun`, `RootPairing.corootSpan_dualAnnihilator_map_eq`, `Dual.transpose_comp`, `RootPairing.corootForm_apply_apply`, `LinearMap.range_dualMap_dual_eq_span_singleton`, `Basis.linearCombination_dualBasis`, `transpose_dualTensorHom`, `FGModuleCat.FGModuleCatDual_obj`, `Submodule.dualCoannihilator_bot`, `QuadraticForm.dualProdIsometry_invFun`, `CliffordAlgebra.contractLeft_contractLeft`, `Submodule.dualCoannihilator_top`, `Dual.instIsReflecive`, `LinearMap.dualMap_injective_of_surjective`, `LinearMap.dualMap_injective_iff`, `LinearEquiv.instIsPerfPair`, `Basis.eval_range`, `CliffordAlgebra.contractLeft_ι_mul`, `LinearMap.dualPairing_nondegenerate`, `Subspace.dualRestrict_leftInverse`, `LinearMap.extendTo𝕜'_apply_re`, `LinearMap.transvection.apply`, `LinearMap.BilinForm.toDual_def`, `CliffordAlgebra.contractRight_mul_algebraMap`, `IsReflexive.bijective_dual_eval'`, `Subspace.flip_quotDualCoannihilatorToDual_bijective`, `Subspace.dual_finrank_eq`, `LieModule.exists_nontrivial_weightSpace_of_isNilpotent`, `Basis.toDual_range`, `PiTensorProduct.dualDistribInvOfBasis_apply`, `TensorProduct.AlgebraTensorModule.dualDistrib_apply`, `Submodule.dualAnnihilator_sup_eq`, `Submodule.dualCoannihilator_sup_eq`, `LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `symm_dualMap_evalEquiv`, `Submodule.dualCopairing_apply`, `dualPairing_apply`, `RootPairing.toPerfPair_flip_comp_coroot`, `nontrivial_dual_iff`, `toMatrix_dualTensorHom`, `LinearMap.dualMap_apply'`, `exteriorPower.ιMultiDual_apply_ιMulti`, `PiTensorProduct.dualDistribEquivOfBasis_apply_apply`, `LinearMap.dualMap_bijective_iff`, `TensorPower.multilinearMapToDual_apply_tprod`, `Basis.sum_dual_apply_smul_coord`, `Basis.toDual_eq_repr`, `exteriorPower.pairingDual_ιMulti_ιMulti`, `LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing`, `eval_apply_eq_zero_iff`, `CliffordAlgebra.contractLeft_comm`, `Basis.toDual_toDual`, `dualProdDualEquivDual_apply_apply`, `Subspace.quotAnnihilatorEquiv_apply`, `RootPairing.rootForm_apply_apply`, `Basis.dualBasis_apply`, `LinearMap.apply_toPerfPair_flip`, `RootPairing.iInf_ker_root'_eq`, `LinearMap.norm_extendTo𝕜'_apply_sq`, `IsBaseChange.toDual_comp_apply`, `RootPairing.PolarizationIn_apply`, `LinearEquiv.dualMap_symm`, `PiTensorProduct.dualDistrib_apply`, `Dual.baseChange_apply_tmul`, `LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg`, `QuadraticForm.dualProdIsometry_toFun`, `IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt`, `Submodule.mem_dualCoannihilator`, `LinearMap.det_dualMap`, `LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux`, `Basis.toDual_injective`, `RootPairing.iInf_ker_coroot'_eq`, `Subspace.finrank_add_finrank_dualCoannihilator_eq`, `dualProdDualEquivDual_apply`, `RootPairing.Hom.weight_coweight_transpose_apply`, `DualBases.eval_same`, `QuadraticForm.toDualProd_apply`, `RootPairing.CoPolarization_apply`, `preReflection_apply`, `DualBases.dual_lc`, `LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective`, `RootPairing.reflection_dualMap_eq_coreflection`, `Subspace.dualLift_of_mem`, `Submodule.dualAnnihilator_gc`, `RootPairing.span_root'_eq_top`, `eval_ker`, `RootPairing.ker_rootForm_eq_dualAnnihilator`, `Submodule.sup_dualAnnihilator_le_inf`, `CliffordAlgebra.contractLeft_ι`, `Subspace.dualAnnihilator_iInf_eq`, `Submodule.quotDualCoannihilatorToDual_injective`, `Basis.eval_injective`, `IsBaseChange.toDual_apply`, `Subspace.dualRestrict_surjective`, `evalEquiv_apply`, `CliffordAlgebra.contractRight_contractRight`, `exteriorPower.alternatingMapToDual_apply_ιMulti`, `dual_rank_eq`, `contractLeft_apply`, `LinearMap.trace_transpose`, `LieModule.exists_nontrivial_weightSpace_of_isSolvable`, `LinearMap.ker_dualMap_eq_dualCoannihilator_range`, `CliffordAlgebra.changeForm_contractLeft`, `LinearEquiv.dualMap_apply`, `LinearMap.finrank_range_dualMap_eq_finrank_range`, `bijective_dual_eval`, `Basis.dualBasis_repr`, `Dual.baseChange_baseChange`, `TensorProduct.dualDistribInvOfBasis_apply`, `RootPairing.root'_apply_apply_mem_of_mem_span`, `dualTensorHom_prodMap_zero`, `Subspace.dualEquivDual_def`, `TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse`, `Basis.toDual_apply`, `Subspace.dualLift_rightInverse`, `dualTensorHomEquivOfBasis_toLinearMap`, `IsBaseChange.dual`, `apply_evalEquiv_symm_apply`, `Submodule.coe_dualAnnihilator_span`, `Projective.exists_dual_eq_one`, `exteriorPower.basis_repr_apply`, `PiTensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse`, `LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace`, `Subspace.dualCopairing_nondegenerate`, `finite_dual_iff`, `dual_projective`, `RootPairing.coreflection_apply`, `Basis.coe_toDual_self`, `Submodule.dualAnnihilator_top`, `LieAlgebra.IsKilling.rootSystem_pairing_apply`, `CliffordAlgebra.contractRight_one`, `dualTensorHomEquivOfBasis_symm_cancel_left`, `LinearMap.IsPerfPair.id`, `LinearMap.transvection.det`, `LieAlgebra.IsKilling.cartanEquivDual_apply_apply`, `Matrix.toPerfectPairing`, `Subspace.map_le_dualAnnihilator_dualAnnihilator`, `RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root'`, `comp_dualTensorHom`, `QuadraticForm.dualProdProdIsometry_toFun`, `RootPairing.algebraMap_coroot'In_apply`, `RootPairing.coroot'_reflection`, `LinearMap.dualMap_apply`, `LinearMap.dualMap_surjective_iff`, `LinearMap.dualMap_def`, `RootPairing.toPerfPair_conj_reflection`, `Dual.apply_one_mul_eq`, `CliffordAlgebra.contractLeft_mul_algebraMap`, `map_dualTensorHom`, `Submodule.range_dualMap_mkQ_eq`, `Subspace.dualLift_injective`, `DualBases.finite`, `LinearMap.transvection.of_left_eq_zero`, `LinearMap.BilinForm.apply_toDual_symm_apply`, `FGModuleCat.FGModuleCatDual_coe`, `CliffordAlgebra.contractLeft_algebraMap_mul`, `contractRight_apply`, `LinearMap.trace_eq_contract_of_basis`, `LinearMap.range_dualMap_le_dualAnnihilator_ker`, `Matrix.toLin_transpose`, `Submodule.finite_dualAnnihilator_iff`, `Basis.toDual_linearCombination_right`, `RootPairing.toPerfPair_flip_conj_coreflection`, `Invertible.bijective`, `Subspace.dualAnnihilator_le_dualAnnihilator_iff`, `Submodule.le_dualAnnihilator_iff_le_dualCoannihilator`, `LieAlgebra.IsKilling.traceForm_coroot`, `FDRep.char_dual`, `FGModuleCat.FGModuleCatEvaluation_apply'`, `Submodule.dualAnnihilator_bot`, `RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm`, `Dual.eval_naturality`, `map_eval_injective`, `Basis.toDualFlip_apply`, `TensorProduct.dualDistrib_apply`, `RootPairing.rootSpan_dualAnnihilator_map_eq`, `evalEquiv_toLinearMap`, `exteriorPower.ιMultiDual_apply_nondiag`, `LinearMap.dualMap_comp_dualMap`, `Basis.toDual_apply_left`, `LinearMap.toPerfPair_apply`, `Basis.toDual_apply_right`, `Submodule.dualAnnihilator_map_linearEquiv_flip_symm`, `Representation.dual_apply`, `DualBases.coeffs_apply`, `Submodule.dualAnnihilator_iSup_eq`, `Submodule.dualAnnihilator_eq_bot_iff`, `PointedCone.mem_maxTensorProduct`, `LinearEquiv.dualMap_refl`, `Dual.congr_apply_apply`, `Representation.dualTensorHom_comm`, `LinearMap.transvection.baseChange`, `Submodule.dualRestrict_apply`, `Submodule.dualAnnihilator_eq_bot_iff'`, `RootPairing.reflection_apply`, `CliffordAlgebra.contractRight_ι`, `Submodule.map_dualCoannihilator_linearEquiv_flip`, `Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk`, `Subspace.map_dualCoannihilator`, `RootPairing.CoPolarizationIn_apply`, `LinearMap.toLinearMap_toPerfPair`, `RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'`, `RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection`, `RootPairing.root_coroot'_eq_pairing`, `Basis.toDual_eq_equivFun`, `dualTensorHomEquivOfBasis_apply`, `Subspace.quotDualCoannihilatorToDual_bijective`, `LinearMap.ker_dualMap_eq_dualAnnihilator_range`, `PiTensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse`, `LinearEquiv.trans_dualMap_symm_flip`, `CliffordAlgebra.contractLeft_one`, `RootPairing.ker_corootForm_eq_dualAnnihilator`, `Subspace.dualAnnihilator_inf_eq`, `IsBaseChange.toDualBaseChange_tmul`, `FDRep.dualTensorIsoLinHom_hom_hom`, `LinearMap.IsPerfectCompl.isCompl_left`, `Submodule.map_dualAnnihilator_linearEquiv_flip_symm`, `SpecialLinearGroup.coe_dualMap`, `Subspace.isCompl_dualAnnihilator`, `Basis.eval_ker`, `Subspace.comap_dualAnnihilator_dualAnnihilator`, `erange_coe`, `LieAlgebra.IsKilling.rootSystem_root_apply`, `Submodule.le_dualCoannihilator_dualAnnihilator`, `contractLeft_assoc_coevaluation'`, `TensorProduct.dualDistribEquivOfBasis_apply_apply`, `dualProdDualEquivDual_symm_apply`, `LinearMap.dualProd.toQuadraticForm`, `Subspace.finrank_add_finrank_dualAnnihilator_eq`, `RootPairing.algebraMap_root'In_apply`, `Submodule.flip_quotDualCoannihilatorToDual_injective`, `Subspace.dualPairing_eq`, `QuadraticForm.dualProdProdIsometry_invFun`, `Basis.coord_toDualEquiv_symm_apply`, `mapEvalEquiv_symm_apply`, `Subspace.dualEquivDual_apply`, `Dual.congr_symm_apply_apply`, `TensorPower.pairingDual_tprod_tprod`, `LinearMap.IsPerfPair.dualEval`, `LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple`, `LinearMap.separatingLeft_dualProd`, `CliffordAlgebra.contractLeft_algebraMap`

NormedSpace

Definitions

Name	Category	Theorems
`inclusionInDoubleDual` 📖	CompOp	4 math math: `inclusionInDoubleDual_norm_eq`, `inclusionInDoubleDual_norm_le`, `double_dual_bound`, `dual_def`
`inclusionInDoubleDualLi` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedBall_inv_subset_polar_closedBall` 📖	mathematical	—	`Set` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `Set.instHasSubset` `Metric.closedBall` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.zero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real` `Real.instInv` `StrongDual.polar` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomIsometric.ids` `ContinuousLinearMap.le_opNorm` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mem_closedBall_zero_iff` `norm_nonneg` `LE.le.trans` `dist_nonneg` `inv_mul_eq_div` `div_self_le_one` `Real.instZeroLEOneClass`
`double_dual_bound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.funLike` `inclusionInDoubleDual` `SeminormedAddCommGroup.toNorm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `RingHomIsometric.ids` `one_mul` `ContinuousLinearMap.le_of_opNorm_le` `inclusionInDoubleDual_norm_le`
`dual_def` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.funLike` `ContinuousLinearMap` `ContinuousLinearMap.addCommGroup` `inclusionInDoubleDual`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul`
`eq_iff_forall_dual_eq` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`sub_eq_zero` `eq_zero_iff_forall_dual_eq_zero` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`eq_zero_iff_forall_dual_eq_zero` 📖	mathematical	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `eq_zero_of_forall_dual_eq_zero`
`eq_zero_of_forall_dual_eq_zero` 📖	mathematical	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`norm_le_zero_iff` `norm_le_dual_bound` `le_rfl` `norm_zero` `MulZeroClass.zero_mul`
`inclusionInDoubleDual_norm_eq` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `inclusionInDoubleDual` `ContinuousLinearMap.id`	—	`ContinuousLinearMap.opNorm_flip` `Algebra.to_smulCommClass` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`inclusionInDoubleDual_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `inclusionInDoubleDual` `Real.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `RingHomIsometric.ids` `inclusionInDoubleDual_norm_eq` `ContinuousLinearMap.norm_id_le`
`isBounded_polar_of_mem_nhds_zero` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	`Bornology.IsBounded` `StrongDual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `AddCommGroup.toAddCommMonoid` `toModule` `PseudoMetricSpace.toBornology` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `StrongDual.polar`	—	`RingHomIsometric.ids` `NormedField.exists_one_lt_norm` `Metric.mem_nhds_iff` `Bornology.IsBounded.subset` `Metric.isBounded_closedBall` `LE.le.trans` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `LinearMap.polar_antitone` `polar_ball_subset_closedBall_div`
`isClosed_polar` 📖	mathematical	—	`IsClosed` `StrongDual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `StrongDual.polar`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Algebra.to_smulCommClass` `LinearMap.polar_eq_iInter` `Set.iInter_congr_Prop` `isClosed_biInter` `IsClosed.preimage` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `toIsBoundedSMul` `Continuous.norm` `ContinuousLinearMap.continuous` `isClosed_Iic` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid`
`norm_le_dual_bound` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instMul` `ContinuousLinearMap.hasOpNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`SeminormedAddCommGroup.toNorm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `RingHomIsometric.ids` `LinearIsometry.norm_map` `ContinuousLinearMap.opNorm_le_bound`
`polar_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StrongDual.polar` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Metric.closedBall` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.zero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instInv`	—	`le_antisymm` `RingHomIsometric.ids` `mem_closedBall_zero_iff` `le_of_forall_gt_imp_ge_of_dense` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `ne_of_lt` `RCLike.norm_of_nonneg` `le_trans` `zero_le_one` `Real.instZeroLEOneClass` `le_of_lt` `inv_lt_iff_one_lt_mul₀'` `polar_ball_subset_closedBall_div` `polar_closedBall` `LinearMap.polar_antitone` `Metric.ball_subset_closedBall`
`polar_ball_subset_closedBall_div` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `Real.instZero`	`Set` `StrongDual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `NormedField.toNormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `Set.instHasSubset` `StrongDual.polar` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Metric.closedBall` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ContinuousLinearMap.zero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`RingHomIsometric.ids` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ContinuousLinearMap.opNorm_le_of_shell` `LT.lt.le` `StrongDual.mem_polar_iff` `inv_le_iff_one_le_mul₀'` `inv_div`
`polar_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`StrongDual.polar` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.zero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instInv`	—	`Set.Subset.antisymm` `RingHomIsometric.ids` `ContinuousLinearMap.opNorm_le_of_ball` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `one_div` `LinearMap.bound_of_ball_bound'` `closedBall_inv_subset_polar_closedBall`
`polar_closure` 📖	mathematical	—	`StrongDual.polar` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toModule` `closure`	—	`LE.le.antisymm` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `LinearMap.polar_antitone` `subset_closure` `GaloisConnection.l_le` `LinearMap.polar_gc` `closure_minimal` `GaloisConnection.le_u_l` `SMulCommClass.symm` `LinearMap.flip_flip` `IsClosed.preimage` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.continuous` `RingHomIsometric.ids` `isClosed_polar`
`sInter_polar_eq_closedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set.sInter` `StrongDual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `Set.image` `Set` `StrongDual.polar` `setOf` `Set.Finite` `Set.instHasSubset` `Metric.closedBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instInv` `ContinuousLinearMap.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.zero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`RingHomIsometric.ids` `inv_inv` `polar_closedBall` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `StrongDual.polar.eq_1` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `LinearMap.sInter_polar_finite_subset_eq_polar`
`smul_mem_polar` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Set` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `Set.instMembership` `StrongDual.polar` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `inv_zero` `zero_smul` `IsTopologicalSemiring.toContinuousAdd` `LinearMap.zero_mem_polar` `norm_smul` `toNormSMulClass` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `le_of_eq` `norm_nonneg` `norm_inv` `inv_mul_cancel₀`

---

← Back to Index