Polar

📁 Source: Mathlib/Analysis/LocallyConvex/Polar.lean

Statistics

Metric	Count
Definitions polar, polarSubmodule, polar, polarSubmodule	4
Theorems mem_polar_singleton, polar_antitone, polar_empty, polar_eq_biInter_preimage, polar_eq_iInter, polar_gc, polar_iUnion, polar_isClosed, polar_mem, polar_mem_iff, polar_nonempty, polar_singleton, polar_subMulAction, polar_union, polar_univ, polar_weak_closed, polar_zero, sInter_polar_finite_subset_eq_polar, subset_bipolar, tripolar_eq_polar, zero_mem_polar, dualPairing_separatingLeft, mem_polarSubmodule, mem_polar_iff, mem_polar_singleton, polarSubmodule_eq_polar, polarSubmodule_eq_setOf, polar_empty, polar_nonempty, polar_singleton, polar_univ, polar_zero, zero_mem_polar	33
Total	37

LinearMap

Definitions

Name	Category	Theorems
polar 📖	CompOp	21 math math: subset_bipolar, polar_iUnion, polar_eq_iInter, polar_antitone, polar_singleton, zero_mem_polar, polar_empty, polar_gc, polar_weak_closed, sInter_polar_finite_subset_eq_polar, mem_polar_singleton, polar_AbsConvex, polar_eq_biInter_preimage, tripolar_eq_polar, polar_univ, polar_subMulAction, polar_union, polar_isClosed, polar_nonempty, polar_zero, polar_mem_iff
polarSubmodule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_polar_singleton 📖	mathematical	—	Set Set.instMembership polar Set.instSingletonSet Real Real.instLE Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Real.instOne	—	Algebra.to_smulCommClass polar_singleton
polar_antitone 📖	mathematical	—	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra polar	—	Algebra.to_smulCommClass GaloisConnection.monotone_l polar_gc
polar_empty 📖	mathematical	—	polar Set Set.instEmptyCollection Set.univ	—	Algebra.to_smulCommClass GaloisConnection.l_bot polar_gc
polar_eq_biInter_preimage 📖	mathematical	—	polar Set.iInter Set Set.instMembership Set.preimage DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Metric.closedBall MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Real Real.instOne	—	Algebra.to_smulCommClass Set.ext dist_zero_right
polar_eq_iInter 📖	mathematical	—	polar Set.iInter Set Set.instMembership setOf Real Real.instLE Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Real.instOne	—	Algebra.to_smulCommClass Set.ext
polar_gc 📖	mathematical	—	GaloisConnection Set OrderDual PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual polar flip CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring OrderDual.ofDual	—	Algebra.to_smulCommClass
polar_iUnion 📖	mathematical	—	polar Set.iUnion Set.iInter	—	Algebra.to_smulCommClass GaloisConnection.l_iSup polar_gc
polar_isClosed 📖	mathematical	—	IsClosed WeakBilin CommRing.toCommSemiring NormedCommRing.toCommRing flip CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring WeakBilin.instTopologicalSpace polar	—	Algebra.to_smulCommClass polar_eq_biInter_preimage isClosed_biInter IsClosed.preimage WeakBilin.eval_continuous Metric.isClosed_closedBall
polar_mem 📖	mathematical	Set Set.instMembership polar	Real Real.instLE Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Real.instOne	—	Algebra.to_smulCommClass
polar_mem_iff 📖	mathematical	—	Set Set.instMembership polar Real Real.instLE Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Real.instOne	—	Algebra.to_smulCommClass
polar_nonempty 📖	mathematical	—	Set.Nonempty polar	—	Algebra.to_smulCommClass zero_mem_polar
polar_singleton 📖	mathematical	—	polar Set Set.instSingletonSet setOf Real Real.instLE Norm.norm NormedRing.toNorm NormedCommRing.toNormedRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Real.instOne	—	Algebra.to_smulCommClass le_antisymm polar_mem_iff Set.mem_singleton_iff
polar_subMulAction 📖	mathematical	—	polar NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SetLike.coe setOf	—	Algebra.to_smulCommClass Set.ext NormedField.exists_lt_norm Mathlib.Tactic.Contrapose.contrapose₁ one_div le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass norm_mul NormedDivisionRing.toNormMulClass SMulMemClass.smul_mem norm_zero Real.instZeroLEOneClass
polar_union 📖	mathematical	—	polar Set Set.instUnion Set.instInter	—	Algebra.to_smulCommClass GaloisConnection.l_sup polar_gc
polar_univ 📖	mathematical	SeparatingRight Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	polar Set.univ Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Algebra.to_smulCommClass Set.eq_singleton_iff_unique_mem norm_le_zero_iff le_of_forall_gt_imp_ge_of_dense LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NormedField.exists_norm_lt map_smul smul_apply smul_eq_mul norm_mul NormedDivisionRing.toNormMulClass norm_inv mul_inv_cancel_left₀ LT.lt.ne' mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt norm_nonneg mul_one
polar_weak_closed 📖	mathematical	—	IsClosed WeakBilin CommRing.toCommSemiring NormedCommRing.toCommRing flip CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring WeakBilin.instTopologicalSpace polar	—	polar_isClosed
polar_zero 📖	mathematical	—	polar Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.univ	—	Algebra.to_smulCommClass polar_singleton map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass norm_zero Real.instZeroLEOneClass
sInter_polar_finite_subset_eq_polar 📖	mathematical	—	Set.sInter Set.image Set polar setOf Set.Finite Set.instHasSubset	—	Algebra.to_smulCommClass Set.ext Set.sInter_image polar_singleton Set.finite_singleton Set.singleton_subset_iff polar_antitone
subset_bipolar 📖	mathematical	—	Set Set.instHasSubset polar flip CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass SMulCommClass.symm flip_apply
tripolar_eq_polar 📖	mathematical	—	polar flip CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring	—	Algebra.to_smulCommClass LE.le.antisymm polar_antitone subset_bipolar
zero_mem_polar 📖	mathematical	—	Set Set.instMembership polar AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Algebra.to_smulCommClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass norm_zero Real.instZeroLEOneClass

StrongDual

Definitions

Name	Category	Theorems
polar 📖	CompOp	19 math math: NormedSpace.isBounded_polar_of_mem_nhds_zero, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, NormedSpace.isClosed_polar, NormedSpace.smul_mem_polar, NormedSpace.polar_ball_subset_closedBall_div, polarSubmodule_eq_polar, NormedSpace.polar_closure, polar_univ, NormedSpace.polar_ball, NormedSpace.sInter_polar_eq_closedBall, zero_mem_polar, polar_empty, NormedSpace.closedBall_inv_subset_polar_closedBall, polar_zero, mem_polar_iff, NormedSpace.polar_closedBall, polar_singleton, mem_polar_singleton, polar_nonempty
polarSubmodule 📖	CompOp	3 math math: polarSubmodule_eq_setOf, polarSubmodule_eq_polar, mem_polarSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualPairing_separatingLeft 📖	mathematical	—	LinearMap.SeparatingLeft ContinuousLinearMap CommSemiring.toSemiring CommRing.toCommSemiring SeminormedCommRing.toCommRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalSeminormedCommRing.toNonUnitalCommRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Ring.uniformContinuousConstSMul SeminormedRing.toRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing topDualPairing	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul smulCommClass_self LinearMap.separatingLeft_iff_ker_eq_bot SeminormedAddCommGroup.toIsTopologicalAddGroup LinearMap.ker_eq_bot ContinuousLinearMap.coe_injective
mem_polarSubmodule 📖	mathematical	—	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Submodule ContinuousLinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing 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 SetLike.instMembership Submodule.setLike polarSubmodule DFunLike.coe ContinuousLinearMap.funLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul polarSubmodule_eq_setOf
mem_polar_iff 📖	mathematical	—	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Set CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.instMembership polar Real Real.instLE Norm.norm NormedField.toNorm DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instOne	—	—
mem_polar_singleton 📖	mathematical	—	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Set CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.instMembership polar Set.instSingletonSet Real Real.instLE Norm.norm NormedField.toNorm DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instOne	—	polar_singleton
polarSubmodule_eq_polar 📖	mathematical	—	SetLike.coe Submodule StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing 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 Submodule.setLike polarSubmodule SubMulAction SubMulAction.instSetLike SubMulAction.instSMulMemClass polar	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul SubMulAction.instSMulMemClass
polarSubmodule_eq_setOf 📖	mathematical	—	SetLike.coe Submodule StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing 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 Submodule.setLike polarSubmodule setOf	—	LinearMap.polar_subMulAction IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul
polar_empty 📖	mathematical	—	polar NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instEmptyCollection Set.univ StrongDual CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	—	LinearMap.polar_empty
polar_nonempty 📖	mathematical	—	Set.Nonempty StrongDual CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing polar	—	LinearMap.polar_nonempty
polar_singleton 📖	mathematical	—	polar NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instSingletonSet setOf StrongDual CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real Real.instLE Norm.norm NormedField.toNorm DFunLike.coe ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instOne	—	LinearMap.polar_singleton
polar_univ 📖	mathematical	—	polar NormedField.toNormedCommRing NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid Set.univ StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Set CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.instSingletonSet ContinuousLinearMap.zero RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	LinearMap.polar_univ IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul smulCommClass_self LinearMap.flip_separatingRight dualPairing_separatingLeft
polar_zero 📖	mathematical	—	polar NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.univ StrongDual CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	—	LinearMap.polar_zero
zero_mem_polar 📖	mathematical	—	StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Set CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.instMembership polar ContinuousLinearMap.zero RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	LinearMap.zero_mem_polar

---

← Back to Index