ValuativeRel

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

Statistics

Metric	Count
Definitions instValuedValueGroupWithZeroOfIsUniformAddGroup, ValuativeRel, «term𝒪[_]», «term𝓀[_]», «term𝓂[_]»	5
Theorems continuous_valuation, hasBasis_nhds, hasBasis_nhds', hasBasis_nhds_zero, hasBasis_nhds_zero', instIsTopologicalRing, isClopen_ball, isClopen_closedBall, isClopen_sphere, isClosed_ball, isClosed_closedBall, isOpen_ball, isOpen_closedBall, isOpen_sphere, isTopologicalAddGroup, mem_nhds_iff', mem_nhds_zero_iff, of_zero, v_eq_valuation	19
Total	24

IsValuativeTopology

Definitions

Name	Category	Theorems
instValuedValueGroupWithZeroOfIsUniformAddGroup 📖	CompOp	2 math math: v_eq_valuation, IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_valuation 📖	mathematical	—	Continuous ValuativeRel.ValueGroupWithZero WithZeroTopology.topologicalSpace ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	Filter.HasBasis.tendsto_iff hasBasis_nhds WithZeroTopology.hasBasis_nhds_zero Valuation.map_sub_of_right_eq_zero WithZeroTopology.hasBasis_nhds_of_ne_zero Valuation.map_eq_of_sub_lt
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
instIsTopologicalRing 📖	mathematical	—	IsTopologicalRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Valued.instIsTopologicalRing isTopologicalAddGroup isUniformAddGroup_of_addCommGroup
isClopen_ball 📖	mathematical	—	IsClopen setOf ValuativeRel.ValueGroupWithZero 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	—	isClosed_ball isOpen_ball
isClopen_closedBall 📖	mathematical	—	IsClopen setOf ValuativeRel.ValueGroupWithZero ValuativeRel.instLEValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	isClosed_closedBall isOpen_closedBall
isClopen_sphere 📖	mathematical	—	IsClopen setOf ValuativeRel.ValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	Set.ext IsClopen.diff isClopen_closedBall isClopen_ball
isClosed_ball 📖	mathematical	—	IsClosed setOf ValuativeRel.ValueGroupWithZero 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	—	eq_or_ne AddSubgroup.isClosed_of_isOpen IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRing isOpen_ball
isClosed_closedBall 📖	mathematical	—	IsClosed setOf ValuativeRel.ValueGroupWithZero ValuativeRel.instLEValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	isOpen_compl_iff isOpen_iff_mem_nhds mem_nhds_iff' ne_of_gt lt_of_le_of_lt zero_le' ne_of_lt Valuation.map_sub_eq_of_lt_left Valuation.map_sub_swap
isOpen_ball 📖	mathematical	—	IsOpen setOf ValuativeRel.ValueGroupWithZero 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	—	isOpen_iff_mem_nhds eq_or_ne nhds_neBot mem_nhds_iff' LE.le.trans_lt Valuation.map_add max_lt sub_add_cancel
isOpen_closedBall 📖	mathematical	—	IsOpen setOf ValuativeRel.ValueGroupWithZero ValuativeRel.instLEValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	isOpen_iff_mem_nhds mem_nhds_iff' le_trans Valuation.map_add max_le le_of_lt sub_add_cancel
isOpen_sphere 📖	mathematical	—	IsOpen setOf ValuativeRel.ValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	IsClopen.isOpen isClopen_sphere
isTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	continuous_iff_continuousAt Filter.HasBasis.tendsto_iff hasBasis_nhds add_sub_add_left_eq_sub 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
mem_nhds_iff' 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.instHasSubset setOf ValuativeRel.ValueGroupWithZero 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 Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	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 Set.instHasSubset setOf ValuativeRel.ValueGroupWithZero 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 Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	sub_zero mem_nhds_iff'
of_zero 📖	mathematical	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.instHasSubset setOf ValuativeRel.ValueGroupWithZero 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 Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	IsValuativeTopology	—	vadd_mem_nhds_vadd_iff neg_add_cancel Set.image_congr Set.image_add_left neg_neg
v_eq_valuation 📖	mathematical	—	Valued.v CommRing.toRing ValuativeRel.ValueGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero instValuedValueGroupWithZeroOfIsUniformAddGroup ValuativeRel.valuation	—	—

ValuativeRel

Definitions

Name	Category	Theorems
«term𝒪[_]» 📖	CompOp	—
«term𝓀[_]» 📖	CompOp	—
«term𝓂[_]» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ValuativeRel 📖	CompData	—

---

← Back to Index