Commit 2023-02-28 04:45 917b7089

View on Github →

feat: define UniformSpace.ofFun (#2511) Forward-port leanprover-community/mathlib#18495

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

added def AbsoluteValue.Simps.apply

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.tendsto_infᵢ_infᵢ

added theorem Filter.tendsto_supᵢ_supᵢ

Modified Mathlib/Topology/UniformSpace/AbsoluteValue.lean

added theorem AbsoluteValue.hasBasis_uniformity

added def AbsoluteValue.uniformSpace

deleted theorem IsAbsoluteValue.mem_uniformity

deleted def IsAbsoluteValue.uniformSpace

deleted def IsAbsoluteValue.uniformSpaceCore

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem UniformSpace.hasBasis_ofFun

added def UniformSpace.ofFun