ValuationTopology

📁 Source: Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

Statistics

Metric	Count
Definitions Valued, mk', toUniformSpace, v	4
Theorems map_eq_one_of_forall_lt, subgroups_basis, cauchy_iff, discreteTopology_of_forall_lt, discreteTopology_of_forall_map_eq_one, hasBasis_nhds_zero, hasBasis_uniformity, instIsTopologicalRing, isClopen_ball, isClopen_closedBall, isClopen_integer, isClopen_sphere, isClopen_valuationSubring, isClosed_ball, isClosed_closedBall, isClosed_integer, isClosed_sphere, isClosed_valuationSubring, isOpen_ball, isOpen_closedBall, isOpen_closedball, isOpen_integer, isOpen_sphere, isOpen_valuationSubring, is_topological_valuation, loc_const, mem_nhds, mem_nhds_zero, toIsUniformAddGroup, toUniformSpace_eq	30
Total	34

Valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_one_of_forall_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing instFunLike	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	CanLift.prf instCanLiftUnitsValIsUnit lt_trichotomy exists_pow_lt Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid Units.instMulArchimedean MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass LT.lt.not_gt map_pow isReduced_of_noZeroDivisors GroupWithZero.noZeroDivisors GroupWithZero.toNontrivial inv_lt_one' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono inv_pow Units.val_inv_eq_inv_val zpow_neg zpow_natCast map_inv₀
subgroups_basis 📖	mathematical	—	RingSubgroupsBasis Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ltAddSubgroup	—	Units.min_val exists_square_le IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid map_mul mul_lt_mul'' LinearOrderedCommMonoidWithZero.toPosMulStrictMono MulPosStrictMono.toMulPosMono LinearOrderedCommMonoidWithZero.toMulPosStrictMono zero_le' GroupWithZero.eq_zero_or_unit MulZeroClass.zero_mul Units.zero_lt mul_comm Units.val_inv_eq_inv_val inv_inv mul_inv_lt_of_lt_mul₀ Units.val_mul MulZeroClass.mul_zero

Valued

Definitions

Name	Category	Theorems
mk' 📖	CompOp	—
toUniformSpace 📖	CompOp	130 math math: continuous_extension, isOpen_closedball, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, extension_extends, valuedCompletion_surjective_iff, PadicComplex.valuation_extends, PadicComplex.coe_eq, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, toUniformSpace_eq, PadicComplex.norm_def, Valuation.IsEquiv.valuedCompletion_le_one_iff, PadicComplex.coe_natCast, isClopen_ball, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', exists_coe_eq_v, NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, is_topological_valuation, continuous_valuation, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, extension_eq_zero_iff, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, tendsto_zero_pow_of_le_exp_neg_one, isClopen_valuationSubring, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, tendsto_zero_pow_of_v_lt_one, isOpen_sphere, isClosed_valuationSubring, Valuation.IsEquiv.uniformContinuous_equivWithVal, instIsTopologicalRing, hasBasis_nhds_zero, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, toIsUniformAddGroup, discreteTopology_of_forall_lt, NumberField.FinitePlace.norm_lt_one_iff_mem, continuous_extensionValuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', isClosed_ball, PadicAlgCl.instUniformContinuousConstSMulPadic, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, isClopen_sphere, PadicComplex.valuation_p, isClosed_sphere, ValuedRing.separated, PadicComplex.isNonarchimedean, isOpen_valuationSubring, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, closure_coe_completion_v_lt, valuation_isClosedMap, closure_coe_completion_v_mul_v_lt, valuedCompletion_apply, cauchy_iff, NumberField.FinitePlace.norm_def_int, isClosed_integer, integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, PadicComplex.instIsScalarTowerPadicPadicAlgCl, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, isClopen_integer, LaurentSeries.valuation_LaurentSeries_equal_extension, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicComplex.coe_zero, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, integer.properSpace_iff_compactSpace_integer, isOpen_closedBall, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, mem_nhds_zero, isOpen_ball, mem_nhds, extensionValuation_apply_coe, LaurentSeries.instLaurentSeriesComplete, discreteTopology_of_forall_map_eq_one, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, isOpen_integer, LaurentSeries.tendsto_valuation, PadicComplex.norm_extends, LaurentSeries.coe_range_dense, completable, Padic.coe_withValRingEquiv_symm, LaurentSeries.comparePkg_eq_extension, hasBasis_uniformity, PadicComplex.rankOne_hom_eq, instFaithfulSMulCompletionOfUniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, LaurentSeries.uniformContinuous_coeff, isClosed_closedBall, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, integer.totallyBounded_iff_finite_residueField, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, loc_const, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, isClopen_closedBall, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, PadicComplex.nnnorm_extends, isTopologicalDivisionRing, Padic.isDenseInducing_cast_withVal, PadicComplexInt.integers, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
v 📖	CompOp	88 math math: isOpen_closedball, Padic.withValUniformEquiv_norm_le_one_iff, toNormedField.norm_le_one_iff, extension_extends, valuedCompletion_surjective_iff, PadicComplex.valuation_extends, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, LaurentSeries.valuation_single_zpow, toUniformSpace_eq, Valuation.IsEquiv.valuedCompletion_le_one_iff, isClopen_ball, exists_coe_eq_v, is_topological_valuation, continuous_valuation, WithVal.apply_symm_equiv, LaurentSeries.val_le_one_iff_eq_coe, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, FunctionField.valuedFqtInfty.def, isClopen_valuationSubring, WithVal.apply_equiv, isOpen_sphere, isClosed_valuationSubring, LaurentSeries.exists_ratFunc_val_lt, hasBasis_nhds_zero, coe_valuation_eq_rankOne_hom_comp_valuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', isClosed_ball, isClopen_sphere, PadicAlgCl.valuation_p, PadicComplex.valuation_p, isClosed_sphere, isOpen_valuationSubring, toNormedField.norm_le_iff, integer.mulArchimedean_mrange_of_isCompact_integer, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, closure_coe_completion_v_lt, valuation_isClosedMap, closure_coe_completion_v_mul_v_lt, valuedCompletion_apply, cauchy_iff, norm_def, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, isClosed_integer, toNormedField.one_lt_norm_iff, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, isClopen_integer, LaurentSeries.valuation_LaurentSeries_equal_extension, RatFunc.v_def, PadicAlgCl.valuation_def, PadicAlgCl.valuation_coe, FunctionField.inftyValuedFqt.def, isOpen_closedBall, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, mem_nhds_zero, isOpen_ball, NormedField.v_eq_valuation, mem_nhds, integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, extensionValuation_apply_coe, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.valuation_compare, isOpen_integer, LaurentSeries.tendsto_valuation, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', IsValuativeTopology.v_eq_valuation, toNormedField.norm_lt_iff, NumberField.toNNReal_valued_eq_adicAbv, hasBasis_uniformity, PadicComplex.rankOne_hom_eq, LaurentSeries.valuation_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, toNormedField.setOf_mem_integer_eq_closedBall, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV, isClosed_closedBall, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, loc_const, isClopen_closedBall, norm_pos_iff_valuation_pos, toNormedField.norm_lt_one_iff, LaurentSeries.exists_ratFunc_eq_v, toNormedField.one_le_norm_iff, PadicComplexInt.integers, LaurentSeries.valuation_X_pow, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_iff 📖	mathematical	—	Cauchy toUniformSpace Filter.NeBot Set Filter Filter.instMembership Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup toUniformSpace_eq AddGroupFilterBasis.cauchy_iff RingSubgroupsBasis.mem_addGroupFilterBasis_iff RingSubgroupsBasis.mem_addGroupFilterBasis
discreteTopology_of_forall_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Valuation.instFunLike v	DiscreteTopology UniformSpace.toTopologicalSpace toUniformSpace	—	discreteTopology_of_forall_map_eq_one GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valuation.map_eq_one_of_forall_lt
discreteTopology_of_forall_map_eq_one 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	DiscreteTopology UniformSpace.toTopologicalSpace toUniformSpace	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRing Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.ne
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v Units.val	—	—
hasBasis_uniformity 📖	mathematical	—	Filter.HasBasis Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero uniformity toUniformSpace setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup toIsUniformAddGroup Filter.HasBasis.comap hasBasis_nhds_zero
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing UniformSpace.toTopologicalSpace toUniformSpace NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup RingFilterBasis.isTopologicalRing toUniformSpace_eq
isClopen_ball 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isClosed_ball isOpen_ball
isClopen_closedBall 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isClosed_closedBall isOpen_closedBall
isClopen_integer 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Subring.instSetLike Valuation.integer v	—	isClosed_integer isOpen_integer
isClopen_sphere 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	Set.ext IsClopen.diff isClopen_closedBall isClopen_ball
isClopen_valuationSubring 📖	mathematical	—	IsClopen UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isClopen_integer
isClosed_ball 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	eq_or_ne AddSubgroup.isClosed_of_isOpen IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRing isOpen_ball
isClosed_closedBall 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isOpen_compl_iff isOpen_iff_mem_nhds mem_nhds ne_of_gt lt_of_le_of_lt zero_le' lt_of_not_ge ne_of_lt Valuation.map_sub_eq_of_lt_left Valuation.map_sub_swap
isClosed_integer 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Subring.instSetLike Valuation.integer v	—	isClosed_closedBall
isClosed_sphere 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	eq_or_ne isClosed_closedBall IsClopen.isClosed isClopen_sphere
isClosed_valuationSubring 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isClosed_integer
isOpen_ball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isOpen_iff_mem_nhds eq_or_ne nhds_neBot mem_nhds LE.le.trans_lt Valuation.map_add max_lt sub_add_cancel
isOpen_closedBall 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isOpen_iff_mem_nhds mem_nhds le_trans Valuation.map_add max_le le_of_lt sub_add_cancel
isOpen_closedball 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v	—	isOpen_closedBall
isOpen_integer 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace SetLike.coe Subring Subring.instSetLike Valuation.integer v	—	isOpen_closedBall one_ne_zero NeZero.one GroupWithZero.toNontrivial
isOpen_sphere 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	IsClopen.isOpen isClopen_sphere
isOpen_valuationSubring 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace toUniformSpace DivisionRing.toRing Field.toDivisionRing SetLike.coe ValuationSubring ValuationSubring.instSetLike Valuation.valuationSubring v	—	isOpen_integer
is_topological_valuation 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
loc_const 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike v	—	mem_nhds Units.val_mk0 Valuation.map_eq_of_sub_lt
mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	nhds_translation_add_neg IsUniformAddGroup.to_topologicalAddGroup toIsUniformAddGroup Filter.HasBasis.mem_iff Filter.HasBasis.comap hasBasis_nhds_zero
mem_nhds_zero 📖	mathematical	—	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	sub_zero
toIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup toUniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
toUniformSpace_eq 📖	mathematical	—	toUniformSpace IsTopologicalAddGroup.rightUniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne RingSubgroupsBasis.topology Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Units.instInhabited Valuation.ltAddSubgroup v Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup RingFilterBasis.toAddGroupFilterBasis RingSubgroupsBasis.toRingFilterBasis	—	UniformSpace.ext Valuation.subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup Filter.HasBasis.eq_of_same_basis hasBasis_uniformity Filter.HasBasis.comap RingSubgroupsBasis.hasBasis_nhds_zero

(root)

Definitions

Name	Category	Theorems
Valued 📖	CompData	—

---

← Back to Index