ValuativeTopology

📁 Source: Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean

Statistics

Metric	Count
Definitions IsValuativeTopology, topologicalSpace, uniformSpace	3
Theorems hasBasis_nhds, hasBasis_nhds', hasBasis_nhds_zero, hasBasis_nhds_zero', instIsTopologicalAddGroup, isClopen_ball, isClopen_closedBall, isClopen_sphere, isClosed_ball, isClosed_closedBall, isOpen_ball, isOpen_closedBall, isOpen_sphere, isTopologicalRing, mem_nhds_iff, mem_nhds_iff', mem_nhds_zero_iff, cauchy_iff, discreteTopology_of_forall_lt, discreteTopology_of_forall_map_eq_one, exists_setOf_restrict_le_iff, hasBasis_nhds, hasBasis_nhds_zero, hasBasis_uniformity, 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_integer, isOpen_sphere, isOpen_valuationSubring, is_topological_valuation, locally_const, mem_nhds_iff, mem_nhds_zero_iff, toTopologicalSpace_eq, toUniformSpace_eq, isUniformAddGroup, isValuativeTopology, nonarchimedeanRing	48
Total	51

IsValuativeTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_nhds 📖	mathematical	—	Filter.HasBasis Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero nhds setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	—
hasBasis_nhds' 📖	mathematical	—	Filter.HasBasis ValuativeRel.ValueGroupWithZero nhds ValuativeRel.instZeroValueGroupWithZero setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Filter.HasBasis.to_hasBasis hasBasis_nhds GroupWithZero.toNontrivial Set.instReflSubset
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation Units.val	—	sub_zero hasBasis_nhds
hasBasis_nhds_zero' 📖	mathematical	—	Filter.HasBasis ValuativeRel.ValueGroupWithZero nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ValuativeRel.instZeroValueGroupWithZero setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	Filter.HasBasis.to_hasBasis hasBasis_nhds_zero GroupWithZero.toNontrivial Set.instReflSubset
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	continuous_iff_continuousAt ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valuation.hasBasis_nhds ValuativeRel.instCompatibleValueGroupWithZeroValuation add_sub_add_left_eq_sub Valuation.hasBasis_nhds_zero IsTopologicalAddGroup.of_comm_of_nhds_zero Filter.HasBasis.prod_self Valuation.map_add_lt Valuation.map_neg Filter.map_eq_of_inverse add_neg_cancel_left add_zero Continuous.continuousAt ContinuousConstVAdd.continuous_const_vadd neg_add_cancel
isClopen_ball 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isClopen_ball
isClopen_closedBall 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isClopen_closedBall
isClopen_sphere 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isClopen_sphere
isClosed_ball 📖	mathematical	—	IsClosed setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isClosed_ball
isClosed_closedBall 📖	mathematical	—	IsClosed setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isClosed_closedBall
isOpen_ball 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isOpen_ball
isOpen_closedBall 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isOpen_closedBall
isOpen_sphere 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict	—	Valuation.isOpen_sphere
isTopologicalRing 📖	mathematical	—	IsTopologicalRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Valuation.toTopologicalSpace_eq ValuativeRel.instCompatibleValueGroupWithZeroValuation NonarchimedeanRing.toIsTopologicalRing ValuativeRel.nonarchimedeanRing
mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero Set.instHasSubset Set.image Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation Units.val	—	—
mem_nhds_iff' 📖	mathematical	—	Set Filter Filter.instMembership nhds Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	Set.image_add_left neg_add_eq_sub mem_nhds_iff
mem_nhds_zero_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation Units.val	—	sub_zero

Valuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_iff 📖	mathematical	—	Cauchy Filter.NeBot Set Filter Filter.instMembership MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val CommSemiring.toSemiring CommRing.toCommSemiring WithZero.instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHomClass.toMonoidHomClass 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 Field.toDivisionRing instFunLike	DiscreteTopology	—	discreteTopology_of_forall_map_eq_one GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass map_eq_one_of_forall_lt
discreteTopology_of_forall_map_eq_one 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	DiscreteTopology	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsValuativeTopology.isTopologicalRing mem_nhds_zero_iff Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.ne map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Units.val_one restrict_lt_iff_lt_embedding
exists_setOf_restrict_le_iff 📖	mathematical	—	Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val ValuativeRel.ValueGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero ValuativeRel.instLinearOrderValueGroupWithZero ValuativeRel.valuation	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass OrderMonoidIso.instMulEquivClass
hasBasis_nhds 📖	mathematical	—	Filter.HasBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup nhds setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds_iff
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict Units.val	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass is_topological_valuation
hasBasis_uniformity 📖	mathematical	—	Filter.HasBasis Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup uniformity setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup Filter.HasBasis.comap hasBasis_nhds_zero
isClopen_ball 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isClosed_ball isOpen_ball
isClopen_closedBall 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isClosed_closedBall isOpen_closedBall
isClopen_integer 📖	mathematical	—	IsClopen SetLike.coe Subring Ring.toNonAssocRing CommRing.toRing Subring.instSetLike integer	—	isClosed_integer isOpen_integer
isClopen_sphere 📖	mathematical	—	IsClopen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Set.ext IsClopen.diff isClopen_closedBall isClopen_ball
isClopen_valuationSubring 📖	mathematical	—	IsClopen SetLike.coe ValuationSubring ValuationSubring.instSetLike valuationSubring	—	isClopen_integer
isClosed_ball 📖	mathematical	—	IsClosed setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass eq_or_ne AddSubgroup.isClosed_of_isOpen instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsValuativeTopology.isTopologicalRing isOpen_ball
isClosed_closedBall 📖	mathematical	—	IsClosed setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_compl_iff isOpen_iff_mem_nhds mem_nhds_iff ne_of_gt lt_of_le_of_lt zero_le' ne_of_lt map_sub_eq_of_lt_left map_sub_swap
isClosed_integer 📖	mathematical	—	IsClosed SetLike.coe Subring Ring.toNonAssocRing CommRing.toRing Subring.instSetLike integer	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_le_one_iff isClosed_closedBall
isClosed_sphere 📖	mathematical	—	IsClosed setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass eq_or_ne le_zero_iff isClosed_closedBall IsClopen.isClosed isClopen_sphere
isClosed_valuationSubring 📖	mathematical	—	IsClosed SetLike.coe ValuationSubring ValuationSubring.instSetLike valuationSubring	—	isClosed_integer
isOpen_ball 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_iff_mem_nhds eq_or_ne nhds_neBot mem_nhds_iff LE.le.trans_lt map_add max_lt sub_add_cancel
isOpen_closedBall 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLE WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass isOpen_iff_mem_nhds mem_nhds_iff le_trans map_add max_le le_of_lt sub_add_cancel
isOpen_integer 📖	mathematical	—	IsOpen SetLike.coe Subring Ring.toNonAssocRing CommRing.toRing Subring.instSetLike integer	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict_le_one_iff isOpen_closedBall one_ne_zero NeZero.one WithZero.instNontrivial One.instNonempty
isOpen_sphere 📖	mathematical	—	IsOpen setOf MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass IsClopen.isOpen MonoidWithZeroHom.monoidWithZeroHomClass isClopen_sphere
isOpen_valuationSubring 📖	mathematical	—	IsOpen SetLike.coe ValuationSubring ValuationSubring.instSetLike valuationSubring	—	isOpen_integer
is_topological_valuation 📖	mathematical	—	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict Units.val	—	mem_nhds_zero_iff
locally_const 📖	mathematical	—	Set Filter Filter.instMembership nhds setOf DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds_iff Units.val_mk0 map_eq_of_sub_lt restrict_lt_iff
mem_nhds_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Units.val	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Set.image_add_left neg_add_eq_sub exists_setOf_restrict_le_iff IsValuativeTopology.mem_nhds_iff
mem_nhds_zero_iff 📖	mathematical	—	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Set.instHasSubset setOf MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass Preorder.toLT WithZero.instPreorder Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict Units.val	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass mem_nhds_iff sub_zero
toTopologicalSpace_eq 📖	mathematical	—	RingSubgroupsBasis.topology Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instInhabited ltAddSubgroup DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding subgroups_basis	—	IsValuativeTopology.instIsTopologicalAddGroup ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup toUniformSpace_eq isUniformAddGroup_of_addCommGroup
toUniformSpace_eq 📖	mathematical	—	IsTopologicalAddGroup.rightUniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing RingSubgroupsBasis.topology Units MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZero.toMonoid WithZero.instMonoidWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Units.instInhabited ltAddSubgroup DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map MonoidHomClass.toMonoidHom MonoidWithZeroHom WithZero.instMulZeroOneClass Monoid.toMulOneClass MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup RingFilterBasis.toAddGroupFilterBasis RingSubgroupsBasis.toRingFilterBasis	—	UniformSpace.ext ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass subgroups_basis AddGroupFilterBasis.isTopologicalAddGroup Filter.HasBasis.eq_of_same_basis hasBasis_uniformity sub_eq_add_neg Filter.HasBasis.comap RingSubgroupsBasis.hasBasis_nhds_zero

ValuativeRel

Definitions

Name	Category	Theorems
topologicalSpace 📖	CompOp	2 math math: isValuativeTopology, nonarchimedeanRing
uniformSpace 📖	CompOp	1 math math: isUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUniformAddGroup 📖	mathematical	—	IsUniformAddGroup uniformSpace AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	isUniformAddGroup_of_addCommGroup
isValuativeTopology 📖	mathematical	—	IsValuativeTopology topologicalSpace	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.subgroups_basis Filter.hasBasis_iff RingSubgroupsBasis.hasBasis_nhds Set.image_add_left neg_add_eq_sub Valuation.exists_setOf_restrict_le_iff instCompatibleValueGroupWithZeroValuation
nonarchimedeanRing 📖	mathematical	—	NonarchimedeanRing CommRing.toRing topologicalSpace	—	RingSubgroupsBasis.nonarchimedean ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.subgroups_basis

(root)

Definitions

Name	Category	Theorems
IsValuativeTopology 📖	CompData	3 math math: ValuativeRel.isValuativeTopology, IsValuativeTopology.of_zero, IsNonarchimedeanLocalField.toIsValuativeTopology

---

← Back to Index